H-Termination proof of /home/matraf/haskell/eval_FullyBlown

YES 2.509 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:

↳ HASKELL

  ↳ LR

mainModule Main

((succ :: Enum a => a -> a) :: Enum a => a -> a)

module Main where

import qualified Prelude

Lambda Reductions:
The following Lambda expression

\(m,_)→m

is transformed to

m0 (m,_) = m

The following Lambda expression

\(_,r)→r

is transformed to

r0 (_,r) = r

The following Lambda expression

\(q,_)→q

is transformed to

q1 (q,_) = q

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

mainModule Main

((succ :: Enum a => a -> a) :: Enum a => a -> a)

module Main where

import qualified Prelude

If Reductions:
The following If expression

if primGEqNatS x y then Succ (primDivNatS (primMinusNatS x y) (Succ y)) else Zero

is transformed to

primDivNatS0 x y True = Succ (primDivNatS (primMinusNatS x y) (Succ y))

primDivNatS0 x y False = Zero

The following If expression

if primGEqNatS x y then primModNatS (primMinusNatS x y) (Succ y) else Succ x

is transformed to

primModNatS0 x y True = primModNatS (primMinusNatS x y) (Succ y)

primModNatS0 x y False = Succ x

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

mainModule Main

((succ :: Enum a => a -> a) :: Enum a => a -> a)

module Main where

import qualified Prelude

Replaced joker patterns by fresh variables and removed binding patterns.
Binding Reductions:
The bind variable of the following binding Pattern

frac@(Double vy vz)

is replaced by the following term

Double vy vz

The bind variable of the following binding Pattern

frac@(Float ww wx)

is replaced by the following term

Float ww wx

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

mainModule Main

((succ :: Enum a => a -> a) :: Enum a => a -> a)

module Main where

import qualified Prelude

Cond Reductions:
The following Function with conditions

undefined

| False

= undefined

is transformed to

undefined = undefined1

undefined0 True = undefined

undefined1 = undefined0 False

The following Function with conditions

toEnum 0 = False

toEnum 1 = True

is transformed to

toEnum xz = toEnum3 xz

toEnum xy = toEnum1 xy

toEnum0 True xy = True

toEnum1 xy = toEnum0 (xy == 1) xy

toEnum2 True xz = False

toEnum2 yu yv = toEnum1 yv

toEnum3 xz = toEnum2 (xz == 0) xz

toEnum3 yw = toEnum1 yw

The following Function with conditions

toEnum 0 = ()

is transformed to

toEnum yx = toEnum5 yx

toEnum4 True yx = ()

toEnum5 yx = toEnum4 (yx == 0) yx

The following Function with conditions

toEnum 0 = LT

toEnum 1 = EQ

toEnum 2 = GT

is transformed to

toEnum zx = toEnum11 zx

toEnum yz = toEnum9 yz

toEnum yy = toEnum7 yy

toEnum6 True yy = GT

toEnum7 yy = toEnum6 (yy == 2) yy

toEnum8 True yz = EQ

toEnum8 zu zv = toEnum7 zv

toEnum9 yz = toEnum8 (yz == 1) yz

toEnum9 zw = toEnum7 zw

toEnum10 True zx = LT

toEnum10 zy zz = toEnum9 zz

toEnum11 zx = toEnum10 (zx == 0) zx

toEnum11 vuu = toEnum9 vuu

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

mainModule Main

((succ :: Enum a => a -> a) :: Enum a => a -> a)

module Main where

import qualified Prelude

Let/Where Reductions:
The bindings of the following Let/Where expression

m

where

m = m0 vu6

m0 (m,vv) = m

vu6 = properFraction x

are unpacked to the following functions on top level

truncateVu6 vuv = properFraction vuv

truncateM0 vuv (m,vv) = m

truncateM vuv = truncateM0 vuv (truncateVu6 vuv)

The bindings of the following Let/Where expression

(fromIntegral q,r :% y)

where

q = q1 vu30

q1 (q,xv) = q

r = r0 vu30

r0 (xw,r) = r

vu30 = quotRem x y

are unpacked to the following functions on top level

properFractionR0 vuw vux (xw,r) = r

properFractionQ1 vuw vux (q,xv) = q

properFractionVu30 vuw vux = quotRem vuw vux

properFractionR vuw vux = properFractionR0 vuw vux (properFractionVu30 vuw vux)

properFractionQ vuw vux = properFractionQ1 vuw vux (properFractionVu30 vuw vux)

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

mainModule Main

((succ :: Enum a => a -> a) :: Enum a => a -> a)

module Main where

import qualified Prelude

Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

mainModule Main

(succ :: Enum a => a -> a)

module Main where

import qualified Prelude

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="succ\n  Enum a",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="succ vuy3\n  Enum a",fontsize=16,color="blue",shape="box"];858[label="succ :: Char -> Char",fontsize=10,color="white",style="solid",shape="box"];3 -> 858[label="",style="solid", color="blue", weight=9];
858 -> 4[label="",style="solid", color="blue", weight=3];
859[label="succ :: Double -> Double",fontsize=10,color="white",style="solid",shape="box"];3 -> 859[label="",style="solid", color="blue", weight=9];
859 -> 5[label="",style="solid", color="blue", weight=3];
860[label="succ :: (Ratio a) -> Ratio a",fontsize=10,color="white",style="solid",shape="box"];3 -> 860[label="",style="solid", color="blue", weight=9];
860 -> 6[label="",style="solid", color="blue", weight=3];
861[label="succ :: Integer -> Integer",fontsize=10,color="white",style="solid",shape="box"];3 -> 861[label="",style="solid", color="blue", weight=9];
861 -> 7[label="",style="solid", color="blue", weight=3];
862[label="succ :: Bool -> Bool",fontsize=10,color="white",style="solid",shape="box"];3 -> 862[label="",style="solid", color="blue", weight=9];
862 -> 8[label="",style="solid", color="blue", weight=3];
863[label="succ :: Int -> Int",fontsize=10,color="white",style="solid",shape="box"];3 -> 863[label="",style="solid", color="blue", weight=9];
863 -> 9[label="",style="solid", color="blue", weight=3];
864[label="succ :: () -> ()",fontsize=10,color="white",style="solid",shape="box"];3 -> 864[label="",style="solid", color="blue", weight=9];
864 -> 10[label="",style="solid", color="blue", weight=3];
865[label="succ :: Float -> Float",fontsize=10,color="white",style="solid",shape="box"];3 -> 865[label="",style="solid", color="blue", weight=9];
865 -> 11[label="",style="solid", color="blue", weight=3];
866[label="succ :: Ordering -> Ordering",fontsize=10,color="white",style="solid",shape="box"];3 -> 866[label="",style="solid", color="blue", weight=9];
866 -> 12[label="",style="solid", color="blue", weight=3];
4[label="succ vuy3",fontsize=16,color="black",shape="box"];4 -> 13[label="",style="solid", color="black", weight=3];
5[label="succ vuy3",fontsize=16,color="black",shape="box"];5 -> 14[label="",style="solid", color="black", weight=3];
6[label="succ vuy3\n  Integral a",fontsize=16,color="black",shape="box"];6 -> 15[label="",style="solid", color="black", weight=3];
7[label="succ vuy3",fontsize=16,color="burlywood",shape="box"];867[label="vuy3/Integer vuy30",fontsize=10,color="white",style="solid",shape="box"];7 -> 867[label="",style="solid", color="burlywood", weight=9];
867 -> 16[label="",style="solid", color="burlywood", weight=3];
8[label="succ vuy3",fontsize=16,color="black",shape="box"];8 -> 17[label="",style="solid", color="black", weight=3];
9[label="succ vuy3",fontsize=16,color="burlywood",shape="triangle"];868[label="vuy3/Pos vuy30",fontsize=10,color="white",style="solid",shape="box"];9 -> 868[label="",style="solid", color="burlywood", weight=9];
868 -> 18[label="",style="solid", color="burlywood", weight=3];
869[label="vuy3/Neg vuy30",fontsize=10,color="white",style="solid",shape="box"];9 -> 869[label="",style="solid", color="burlywood", weight=9];
869 -> 19[label="",style="solid", color="burlywood", weight=3];
10[label="succ vuy3",fontsize=16,color="black",shape="box"];10 -> 20[label="",style="solid", color="black", weight=3];
11[label="succ vuy3",fontsize=16,color="black",shape="box"];11 -> 21[label="",style="solid", color="black", weight=3];
12[label="succ vuy3",fontsize=16,color="black",shape="box"];12 -> 22[label="",style="solid", color="black", weight=3];
13[label="toEnum . (Pos (Succ Zero) +) . fromEnum",fontsize=16,color="black",shape="box"];13 -> 23[label="",style="solid", color="black", weight=3];
14[label="toEnum . (Pos (Succ Zero) +) . fromEnum",fontsize=16,color="black",shape="box"];14 -> 24[label="",style="solid", color="black", weight=3];
15[label="toEnum . (Pos (Succ Zero) +) . fromEnum\n  Integral a",fontsize=16,color="black",shape="box"];15 -> 25[label="",style="solid", color="black", weight=3];
16[label="succ (Integer vuy30)",fontsize=16,color="black",shape="box"];16 -> 26[label="",style="solid", color="black", weight=3];
17[label="toEnum . (Pos (Succ Zero) +) . fromEnum",fontsize=16,color="black",shape="box"];17 -> 27[label="",style="solid", color="black", weight=3];
18[label="succ (Pos vuy30)",fontsize=16,color="burlywood",shape="box"];870[label="vuy30/Succ vuy300",fontsize=10,color="white",style="solid",shape="box"];18 -> 870[label="",style="solid", color="burlywood", weight=9];
870 -> 28[label="",style="solid", color="burlywood", weight=3];
871[label="vuy30/Zero",fontsize=10,color="white",style="solid",shape="box"];18 -> 871[label="",style="solid", color="burlywood", weight=9];
871 -> 29[label="",style="solid", color="burlywood", weight=3];
19[label="succ (Neg vuy30)",fontsize=16,color="burlywood",shape="box"];872[label="vuy30/Succ vuy300",fontsize=10,color="white",style="solid",shape="box"];19 -> 872[label="",style="solid", color="burlywood", weight=9];
872 -> 30[label="",style="solid", color="burlywood", weight=3];
873[label="vuy30/Zero",fontsize=10,color="white",style="solid",shape="box"];19 -> 873[label="",style="solid", color="burlywood", weight=9];
873 -> 31[label="",style="solid", color="burlywood", weight=3];
20[label="toEnum . (Pos (Succ Zero) +) . fromEnum",fontsize=16,color="black",shape="box"];20 -> 32[label="",style="solid", color="black", weight=3];
21[label="toEnum . (Pos (Succ Zero) +) . fromEnum",fontsize=16,color="black",shape="box"];21 -> 33[label="",style="solid", color="black", weight=3];
22[label="toEnum . (Pos (Succ Zero) +) . fromEnum",fontsize=16,color="black",shape="box"];22 -> 34[label="",style="solid", color="black", weight=3];
23[label="toEnum ((Pos (Succ Zero) +) . fromEnum)",fontsize=16,color="black",shape="box"];23 -> 35[label="",style="solid", color="black", weight=3];
24[label="toEnum ((Pos (Succ Zero) +) . fromEnum)",fontsize=16,color="black",shape="box"];24 -> 36[label="",style="solid", color="black", weight=3];
25[label="toEnum ((Pos (Succ Zero) +) . fromEnum)\n  Integral a",fontsize=16,color="black",shape="box"];25 -> 37[label="",style="solid", color="black", weight=3];
26[label="Integer (succ vuy30)",fontsize=16,color="green",shape="box"];26 -> 38[label="",style="dashed", color="green", weight=3];
27[label="toEnum ((Pos (Succ Zero) +) . fromEnum)",fontsize=16,color="black",shape="box"];27 -> 39[label="",style="solid", color="black", weight=3];
28[label="succ (Pos (Succ vuy300))",fontsize=16,color="black",shape="box"];28 -> 40[label="",style="solid", color="black", weight=3];
29[label="succ (Pos Zero)",fontsize=16,color="black",shape="box"];29 -> 41[label="",style="solid", color="black", weight=3];
30[label="succ (Neg (Succ vuy300))",fontsize=16,color="black",shape="box"];30 -> 42[label="",style="solid", color="black", weight=3];
31[label="succ (Neg Zero)",fontsize=16,color="black",shape="box"];31 -> 43[label="",style="solid", color="black", weight=3];
32[label="toEnum ((Pos (Succ Zero) +) . fromEnum)",fontsize=16,color="black",shape="box"];32 -> 44[label="",style="solid", color="black", weight=3];
33[label="toEnum ((Pos (Succ Zero) +) . fromEnum)",fontsize=16,color="black",shape="box"];33 -> 45[label="",style="solid", color="black", weight=3];
34[label="toEnum ((Pos (Succ Zero) +) . fromEnum)",fontsize=16,color="black",shape="box"];34 -> 46[label="",style="solid", color="black", weight=3];
35[label="primIntToChar ((Pos (Succ Zero) +) . fromEnum)",fontsize=16,color="black",shape="box"];35 -> 47[label="",style="solid", color="black", weight=3];
36[label="primIntToDouble ((Pos (Succ Zero) +) . fromEnum)",fontsize=16,color="black",shape="box"];36 -> 48[label="",style="solid", color="black", weight=3];
37[label="fromInt ((Pos (Succ Zero) +) . fromEnum)\n  Integral a",fontsize=16,color="black",shape="box"];37 -> 49[label="",style="solid", color="black", weight=3];
38 -> 9[label="",style="dashed", color="red", weight=0];
38[label="succ vuy30",fontsize=16,color="magenta"];38 -> 50[label="",style="dashed", color="magenta", weight=3];
39[label="toEnum3 ((Pos (Succ Zero) +) . fromEnum)",fontsize=16,color="black",shape="box"];39 -> 51[label="",style="solid", color="black", weight=3];
40[label="Pos (Succ (Succ vuy300))",fontsize=16,color="green",shape="box"];41[label="Pos (Succ Zero)",fontsize=16,color="green",shape="box"];42[label="Neg vuy300",fontsize=16,color="green",shape="box"];43[label="Pos (Succ Zero)",fontsize=16,color="green",shape="box"];44[label="toEnum5 ((Pos (Succ Zero) +) . fromEnum)",fontsize=16,color="black",shape="box"];44 -> 52[label="",style="solid", color="black", weight=3];
45[label="primIntToFloat ((Pos (Succ Zero) +) . fromEnum)",fontsize=16,color="black",shape="box"];45 -> 53[label="",style="solid", color="black", weight=3];
46[label="toEnum11 ((Pos (Succ Zero) +) . fromEnum)",fontsize=16,color="black",shape="box"];46 -> 54[label="",style="solid", color="black", weight=3];
47[label="primIntToChar (Pos (Succ Zero) + fromEnum vuy3)",fontsize=16,color="black",shape="box"];47 -> 55[label="",style="solid", color="black", weight=3];
48[label="Double ((Pos (Succ Zero) +) . fromEnum) (Pos (Succ Zero))",fontsize=16,color="green",shape="box"];48 -> 56[label="",style="dashed", color="green", weight=3];
49[label="intToRatio ((Pos (Succ Zero) +) . fromEnum)\n  Integral a",fontsize=16,color="black",shape="box"];49 -> 57[label="",style="solid", color="black", weight=3];
50[label="vuy30",fontsize=16,color="green",shape="box"];51[label="toEnum2 ((Pos (Succ Zero) +) . fromEnum == Pos Zero) ((Pos (Succ Zero) +) . fromEnum)",fontsize=16,color="black",shape="box"];51 -> 58[label="",style="solid", color="black", weight=3];
52[label="toEnum4 ((Pos (Succ Zero) +) . fromEnum == Pos Zero) ((Pos (Succ Zero) +) . fromEnum)",fontsize=16,color="black",shape="box"];52 -> 59[label="",style="solid", color="black", weight=3];
53[label="Float ((Pos (Succ Zero) +) . fromEnum) (Pos (Succ Zero))",fontsize=16,color="green",shape="box"];53 -> 60[label="",style="dashed", color="green", weight=3];
54[label="toEnum10 ((Pos (Succ Zero) +) . fromEnum == Pos Zero) ((Pos (Succ Zero) +) . fromEnum)",fontsize=16,color="black",shape="box"];54 -> 61[label="",style="solid", color="black", weight=3];
55[label="primIntToChar (primPlusInt (Pos (Succ Zero)) (fromEnum vuy3))",fontsize=16,color="black",shape="box"];55 -> 62[label="",style="solid", color="black", weight=3];
56[label="(Pos (Succ Zero) +) . fromEnum",fontsize=16,color="black",shape="box"];56 -> 63[label="",style="solid", color="black", weight=3];
57[label="fromInt ((Pos (Succ Zero) +) . fromEnum) :% fromInt (Pos (Succ Zero))\n  Integral a",fontsize=16,color="green",shape="box"];57 -> 64[label="",style="dashed", color="green", weight=3];
57 -> 65[label="",style="dashed", color="green", weight=3];
58[label="toEnum2 (primEqInt ((Pos (Succ Zero) +) . fromEnum) (Pos Zero)) ((Pos (Succ Zero) +) . fromEnum)",fontsize=16,color="black",shape="box"];58 -> 66[label="",style="solid", color="black", weight=3];
59[label="toEnum4 (primEqInt ((Pos (Succ Zero) +) . fromEnum) (Pos Zero)) ((Pos (Succ Zero) +) . fromEnum)",fontsize=16,color="black",shape="box"];59 -> 67[label="",style="solid", color="black", weight=3];
60[label="(Pos (Succ Zero) +) . fromEnum",fontsize=16,color="black",shape="box"];60 -> 68[label="",style="solid", color="black", weight=3];
61[label="toEnum10 (primEqInt ((Pos (Succ Zero) +) . fromEnum) (Pos Zero)) ((Pos (Succ Zero) +) . fromEnum)",fontsize=16,color="black",shape="box"];61 -> 69[label="",style="solid", color="black", weight=3];
62[label="primIntToChar (primPlusInt (Pos (Succ Zero)) (primCharToInt vuy3))",fontsize=16,color="burlywood",shape="box"];875[label="vuy3/Char vuy30",fontsize=10,color="white",style="solid",shape="box"];62 -> 875[label="",style="solid", color="burlywood", weight=9];
875 -> 70[label="",style="solid", color="burlywood", weight=3];
63[label="Pos (Succ Zero) + fromEnum vuy3",fontsize=16,color="black",shape="box"];63 -> 71[label="",style="solid", color="black", weight=3];
64[label="fromInt ((Pos (Succ Zero) +) . fromEnum)\n  Integral a",fontsize=16,color="blue",shape="box"];876[label="fromInt :: Int -> Int",fontsize=10,color="white",style="solid",shape="box"];64 -> 876[label="",style="solid", color="blue", weight=9];
876 -> 72[label="",style="solid", color="blue", weight=3];
877[label="fromInt :: Int -> Integer",fontsize=10,color="white",style="solid",shape="box"];64 -> 877[label="",style="solid", color="blue", weight=9];
877 -> 73[label="",style="solid", color="blue", weight=3];
65[label="fromInt (Pos (Succ Zero))\n  Integral a",fontsize=16,color="blue",shape="box"];878[label="fromInt :: -> Int Int",fontsize=10,color="white",style="solid",shape="box"];65 -> 878[label="",style="solid", color="blue", weight=9];
878 -> 74[label="",style="solid", color="blue", weight=3];
879[label="fromInt :: -> Int Integer",fontsize=10,color="white",style="solid",shape="box"];65 -> 879[label="",style="solid", color="blue", weight=9];
879 -> 75[label="",style="solid", color="blue", weight=3];
66[label="toEnum2 (primEqInt (Pos (Succ Zero) + fromEnum vuy3) (Pos Zero)) (Pos (Succ Zero) + fromEnum vuy3)",fontsize=16,color="black",shape="box"];66 -> 76[label="",style="solid", color="black", weight=3];
67[label="toEnum4 (primEqInt (Pos (Succ Zero) + fromEnum vuy3) (Pos Zero)) (Pos (Succ Zero) + fromEnum vuy3)",fontsize=16,color="black",shape="box"];67 -> 77[label="",style="solid", color="black", weight=3];
68[label="Pos (Succ Zero) + fromEnum vuy3",fontsize=16,color="black",shape="box"];68 -> 78[label="",style="solid", color="black", weight=3];
69[label="toEnum10 (primEqInt (Pos (Succ Zero) + fromEnum vuy3) (Pos Zero)) (Pos (Succ Zero) + fromEnum vuy3)",fontsize=16,color="black",shape="box"];69 -> 79[label="",style="solid", color="black", weight=3];
70[label="primIntToChar (primPlusInt (Pos (Succ Zero)) (primCharToInt (Char vuy30)))",fontsize=16,color="black",shape="box"];70 -> 80[label="",style="solid", color="black", weight=3];
71[label="primPlusInt (Pos (Succ Zero)) (fromEnum vuy3)",fontsize=16,color="black",shape="box"];71 -> 81[label="",style="solid", color="black", weight=3];
72[label="fromInt ((Pos (Succ Zero) +) . fromEnum)",fontsize=16,color="black",shape="box"];72 -> 82[label="",style="solid", color="black", weight=3];
73[label="fromInt ((Pos (Succ Zero) +) . fromEnum)",fontsize=16,color="black",shape="box"];73 -> 83[label="",style="solid", color="black", weight=3];
74[label="fromInt (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];74 -> 84[label="",style="solid", color="black", weight=3];
75[label="fromInt (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];75 -> 85[label="",style="solid", color="black", weight=3];
76[label="toEnum2 (primEqInt (primPlusInt (Pos (Succ Zero)) (fromEnum vuy3)) (Pos Zero)) (primPlusInt (Pos (Succ Zero)) (fromEnum vuy3))",fontsize=16,color="burlywood",shape="box"];880[label="vuy3/False",fontsize=10,color="white",style="solid",shape="box"];76 -> 880[label="",style="solid", color="burlywood", weight=9];
880 -> 86[label="",style="solid", color="burlywood", weight=3];
881[label="vuy3/True",fontsize=10,color="white",style="solid",shape="box"];76 -> 881[label="",style="solid", color="burlywood", weight=9];
881 -> 87[label="",style="solid", color="burlywood", weight=3];
77[label="toEnum4 (primEqInt (primPlusInt (Pos (Succ Zero)) (fromEnum vuy3)) (Pos Zero)) (primPlusInt (Pos (Succ Zero)) (fromEnum vuy3))",fontsize=16,color="burlywood",shape="box"];882[label="vuy3/()",fontsize=10,color="white",style="solid",shape="box"];77 -> 882[label="",style="solid", color="burlywood", weight=9];
882 -> 88[label="",style="solid", color="burlywood", weight=3];
78[label="primPlusInt (Pos (Succ Zero)) (fromEnum vuy3)",fontsize=16,color="black",shape="box"];78 -> 89[label="",style="solid", color="black", weight=3];
79[label="toEnum10 (primEqInt (primPlusInt (Pos (Succ Zero)) (fromEnum vuy3)) (Pos Zero)) (primPlusInt (Pos (Succ Zero)) (fromEnum vuy3))",fontsize=16,color="burlywood",shape="box"];883[label="vuy3/LT",fontsize=10,color="white",style="solid",shape="box"];79 -> 883[label="",style="solid", color="burlywood", weight=9];
883 -> 90[label="",style="solid", color="burlywood", weight=3];
884[label="vuy3/EQ",fontsize=10,color="white",style="solid",shape="box"];79 -> 884[label="",style="solid", color="burlywood", weight=9];
884 -> 91[label="",style="solid", color="burlywood", weight=3];
885[label="vuy3/GT",fontsize=10,color="white",style="solid",shape="box"];79 -> 885[label="",style="solid", color="burlywood", weight=9];
885 -> 92[label="",style="solid", color="burlywood", weight=3];
80[label="primIntToChar (primPlusInt (Pos (Succ Zero)) (Pos vuy30))",fontsize=16,color="black",shape="box"];80 -> 93[label="",style="solid", color="black", weight=3];
81[label="primPlusInt (Pos (Succ Zero)) (truncate vuy3)",fontsize=16,color="black",shape="box"];81 -> 94[label="",style="solid", color="black", weight=3];
82[label="(Pos (Succ Zero) +) . fromEnum",fontsize=16,color="black",shape="box"];82 -> 95[label="",style="solid", color="black", weight=3];
83[label="Integer ((Pos (Succ Zero) +) . fromEnum)",fontsize=16,color="green",shape="box"];83 -> 96[label="",style="dashed", color="green", weight=3];
84[label="Pos (Succ Zero)",fontsize=16,color="green",shape="box"];85[label="Integer (Pos (Succ Zero))",fontsize=16,color="green",shape="box"];86[label="toEnum2 (primEqInt (primPlusInt (Pos (Succ Zero)) (fromEnum False)) (Pos Zero)) (primPlusInt (Pos (Succ Zero)) (fromEnum False))",fontsize=16,color="black",shape="box"];86 -> 97[label="",style="solid", color="black", weight=3];
87[label="toEnum2 (primEqInt (primPlusInt (Pos (Succ Zero)) (fromEnum True)) (Pos Zero)) (primPlusInt (Pos (Succ Zero)) (fromEnum True))",fontsize=16,color="black",shape="box"];87 -> 98[label="",style="solid", color="black", weight=3];
88[label="toEnum4 (primEqInt (primPlusInt (Pos (Succ Zero)) (fromEnum ())) (Pos Zero)) (primPlusInt (Pos (Succ Zero)) (fromEnum ()))",fontsize=16,color="black",shape="box"];88 -> 99[label="",style="solid", color="black", weight=3];
89[label="primPlusInt (Pos (Succ Zero)) (truncate vuy3)",fontsize=16,color="black",shape="box"];89 -> 100[label="",style="solid", color="black", weight=3];
90[label="toEnum10 (primEqInt (primPlusInt (Pos (Succ Zero)) (fromEnum LT)) (Pos Zero)) (primPlusInt (Pos (Succ Zero)) (fromEnum LT))",fontsize=16,color="black",shape="box"];90 -> 101[label="",style="solid", color="black", weight=3];
91[label="toEnum10 (primEqInt (primPlusInt (Pos (Succ Zero)) (fromEnum EQ)) (Pos Zero)) (primPlusInt (Pos (Succ Zero)) (fromEnum EQ))",fontsize=16,color="black",shape="box"];91 -> 102[label="",style="solid", color="black", weight=3];
92[label="toEnum10 (primEqInt (primPlusInt (Pos (Succ Zero)) (fromEnum GT)) (Pos Zero)) (primPlusInt (Pos (Succ Zero)) (fromEnum GT))",fontsize=16,color="black",shape="box"];92 -> 103[label="",style="solid", color="black", weight=3];
93[label="primIntToChar (Pos (primPlusNat (Succ Zero) vuy30))",fontsize=16,color="black",shape="box"];93 -> 104[label="",style="solid", color="black", weight=3];
94[label="primPlusInt (Pos (Succ Zero)) (truncateM vuy3)",fontsize=16,color="black",shape="box"];94 -> 105[label="",style="solid", color="black", weight=3];
95[label="Pos (Succ Zero) + fromEnum vuy3",fontsize=16,color="black",shape="box"];95 -> 106[label="",style="solid", color="black", weight=3];
96[label="(Pos (Succ Zero) +) . fromEnum",fontsize=16,color="black",shape="box"];96 -> 107[label="",style="solid", color="black", weight=3];
97[label="toEnum2 (primEqInt (primPlusInt (Pos (Succ Zero)) (Pos Zero)) (Pos Zero)) (primPlusInt (Pos (Succ Zero)) (Pos Zero))",fontsize=16,color="black",shape="box"];97 -> 108[label="",style="solid", color="black", weight=3];
98[label="toEnum2 (primEqInt (primPlusInt (Pos (Succ Zero)) (Pos (Succ Zero))) (Pos Zero)) (primPlusInt (Pos (Succ Zero)) (Pos (Succ Zero)))",fontsize=16,color="black",shape="box"];98 -> 109[label="",style="solid", color="black", weight=3];
99[label="toEnum4 (primEqInt (primPlusInt (Pos (Succ Zero)) (Pos Zero)) (Pos Zero)) (primPlusInt (Pos (Succ Zero)) (Pos Zero))",fontsize=16,color="black",shape="box"];99 -> 110[label="",style="solid", color="black", weight=3];
100[label="primPlusInt (Pos (Succ Zero)) (truncateM vuy3)",fontsize=16,color="black",shape="box"];100 -> 111[label="",style="solid", color="black", weight=3];
101[label="toEnum10 (primEqInt (primPlusInt (Pos (Succ Zero)) (Pos Zero)) (Pos Zero)) (primPlusInt (Pos (Succ Zero)) (Pos Zero))",fontsize=16,color="black",shape="box"];101 -> 112[label="",style="solid", color="black", weight=3];
102[label="toEnum10 (primEqInt (primPlusInt (Pos (Succ Zero)) (Pos (Succ Zero))) (Pos Zero)) (primPlusInt (Pos (Succ Zero)) (Pos (Succ Zero)))",fontsize=16,color="black",shape="box"];102 -> 113[label="",style="solid", color="black", weight=3];
103[label="toEnum10 (primEqInt (primPlusInt (Pos (Succ Zero)) (Pos (Succ (Succ Zero)))) (Pos Zero)) (primPlusInt (Pos (Succ Zero)) (Pos (Succ (Succ Zero))))",fontsize=16,color="black",shape="box"];103 -> 114[label="",style="solid", color="black", weight=3];
104[label="Char (primPlusNat (Succ Zero) vuy30)",fontsize=16,color="green",shape="box"];104 -> 115[label="",style="dashed", color="green", weight=3];
105[label="primPlusInt (Pos (Succ Zero)) (truncateM0 vuy3 (truncateVu6 vuy3))",fontsize=16,color="black",shape="box"];105 -> 116[label="",style="solid", color="black", weight=3];
106[label="primPlusInt (Pos (Succ Zero)) (fromEnum vuy3)",fontsize=16,color="black",shape="box"];106 -> 117[label="",style="solid", color="black", weight=3];
107[label="Pos (Succ Zero) + fromEnum vuy3",fontsize=16,color="black",shape="box"];107 -> 118[label="",style="solid", color="black", weight=3];
108[label="toEnum2 (primEqInt (Pos (primPlusNat (Succ Zero) Zero)) (Pos Zero)) (Pos (primPlusNat (Succ Zero) Zero))",fontsize=16,color="black",shape="box"];108 -> 119[label="",style="solid", color="black", weight=3];
109[label="toEnum2 (primEqInt (Pos (primPlusNat (Succ Zero) (Succ Zero))) (Pos Zero)) (Pos (primPlusNat (Succ Zero) (Succ Zero)))",fontsize=16,color="black",shape="box"];109 -> 120[label="",style="solid", color="black", weight=3];
110[label="toEnum4 (primEqInt (Pos (primPlusNat (Succ Zero) Zero)) (Pos Zero)) (Pos (primPlusNat (Succ Zero) Zero))",fontsize=16,color="black",shape="box"];110 -> 121[label="",style="solid", color="black", weight=3];
111[label="primPlusInt (Pos (Succ Zero)) (truncateM0 vuy3 (truncateVu6 vuy3))",fontsize=16,color="black",shape="box"];111 -> 122[label="",style="solid", color="black", weight=3];
112[label="toEnum10 (primEqInt (Pos (primPlusNat (Succ Zero) Zero)) (Pos Zero)) (Pos (primPlusNat (Succ Zero) Zero))",fontsize=16,color="black",shape="box"];112 -> 123[label="",style="solid", color="black", weight=3];
113[label="toEnum10 (primEqInt (Pos (primPlusNat (Succ Zero) (Succ Zero))) (Pos Zero)) (Pos (primPlusNat (Succ Zero) (Succ Zero)))",fontsize=16,color="black",shape="box"];113 -> 124[label="",style="solid", color="black", weight=3];
114[label="toEnum10 (primEqInt (Pos (primPlusNat (Succ Zero) (Succ (Succ Zero)))) (Pos Zero)) (Pos (primPlusNat (Succ Zero) (Succ (Succ Zero))))",fontsize=16,color="black",shape="box"];114 -> 125[label="",style="solid", color="black", weight=3];
115[label="primPlusNat (Succ Zero) vuy30",fontsize=16,color="burlywood",shape="triangle"];886[label="vuy30/Succ vuy300",fontsize=10,color="white",style="solid",shape="box"];115 -> 886[label="",style="solid", color="burlywood", weight=9];
886 -> 126[label="",style="solid", color="burlywood", weight=3];
887[label="vuy30/Zero",fontsize=10,color="white",style="solid",shape="box"];115 -> 887[label="",style="solid", color="burlywood", weight=9];
887 -> 127[label="",style="solid", color="burlywood", weight=3];
116[label="primPlusInt (Pos (Succ Zero)) (truncateM0 vuy3 (properFraction vuy3))",fontsize=16,color="black",shape="box"];116 -> 128[label="",style="solid", color="black", weight=3];
117[label="primPlusInt (Pos (Succ Zero)) (truncate vuy3)",fontsize=16,color="black",shape="box"];117 -> 129[label="",style="solid", color="black", weight=3];
118[label="primPlusInt (Pos (Succ Zero)) (fromEnum vuy3)",fontsize=16,color="black",shape="box"];118 -> 130[label="",style="solid", color="black", weight=3];
119[label="toEnum2 (primEqInt (Pos (Succ Zero)) (Pos Zero)) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];119 -> 131[label="",style="solid", color="black", weight=3];
120[label="toEnum2 (primEqInt (Pos (Succ (Succ (primPlusNat Zero Zero)))) (Pos Zero)) (Pos (Succ (Succ (primPlusNat Zero Zero))))",fontsize=16,color="black",shape="box"];120 -> 132[label="",style="solid", color="black", weight=3];
121[label="toEnum4 (primEqInt (Pos (Succ Zero)) (Pos Zero)) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];121 -> 133[label="",style="solid", color="black", weight=3];
122[label="primPlusInt (Pos (Succ Zero)) (truncateM0 vuy3 (properFraction vuy3))",fontsize=16,color="black",shape="box"];122 -> 134[label="",style="solid", color="black", weight=3];
123[label="toEnum10 (primEqInt (Pos (Succ Zero)) (Pos Zero)) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];123 -> 135[label="",style="solid", color="black", weight=3];
124[label="toEnum10 (primEqInt (Pos (Succ (Succ (primPlusNat Zero Zero)))) (Pos Zero)) (Pos (Succ (Succ (primPlusNat Zero Zero))))",fontsize=16,color="black",shape="box"];124 -> 136[label="",style="solid", color="black", weight=3];
125[label="toEnum10 (primEqInt (Pos (Succ (Succ (primPlusNat Zero (Succ Zero))))) (Pos Zero)) (Pos (Succ (Succ (primPlusNat Zero (Succ Zero)))))",fontsize=16,color="black",shape="box"];125 -> 137[label="",style="solid", color="black", weight=3];
126[label="primPlusNat (Succ Zero) (Succ vuy300)",fontsize=16,color="black",shape="box"];126 -> 138[label="",style="solid", color="black", weight=3];
127[label="primPlusNat (Succ Zero) Zero",fontsize=16,color="black",shape="box"];127 -> 139[label="",style="solid", color="black", weight=3];
128[label="primPlusInt (Pos (Succ Zero)) (truncateM0 vuy3 (floatProperFractionDouble vuy3))",fontsize=16,color="burlywood",shape="box"];888[label="vuy3/Double vuy30 vuy31",fontsize=10,color="white",style="solid",shape="box"];128 -> 888[label="",style="solid", color="burlywood", weight=9];
888 -> 140[label="",style="solid", color="burlywood", weight=3];
129[label="primPlusInt (Pos (Succ Zero)) (truncateM vuy3)",fontsize=16,color="black",shape="box"];129 -> 141[label="",style="solid", color="black", weight=3];
130[label="primPlusInt (Pos (Succ Zero)) (truncate vuy3)",fontsize=16,color="black",shape="box"];130 -> 142[label="",style="solid", color="black", weight=3];
131[label="toEnum2 False (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];131 -> 143[label="",style="solid", color="black", weight=3];
132[label="toEnum2 False (Pos (Succ (Succ (primPlusNat Zero Zero))))",fontsize=16,color="black",shape="box"];132 -> 144[label="",style="solid", color="black", weight=3];
133[label="toEnum4 False (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];133 -> 145[label="",style="solid", color="black", weight=3];
134[label="primPlusInt (Pos (Succ Zero)) (truncateM0 vuy3 (floatProperFractionFloat vuy3))",fontsize=16,color="burlywood",shape="box"];889[label="vuy3/Float vuy30 vuy31",fontsize=10,color="white",style="solid",shape="box"];134 -> 889[label="",style="solid", color="burlywood", weight=9];
889 -> 146[label="",style="solid", color="burlywood", weight=3];
135[label="toEnum10 False (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];135 -> 147[label="",style="solid", color="black", weight=3];
136[label="toEnum10 False (Pos (Succ (Succ (primPlusNat Zero Zero))))",fontsize=16,color="black",shape="box"];136 -> 148[label="",style="solid", color="black", weight=3];
137[label="toEnum10 False (Pos (Succ (Succ (primPlusNat Zero (Succ Zero)))))",fontsize=16,color="black",shape="box"];137 -> 149[label="",style="solid", color="black", weight=3];
138[label="Succ (Succ (primPlusNat Zero vuy300))",fontsize=16,color="green",shape="box"];138 -> 150[label="",style="dashed", color="green", weight=3];
139[label="Succ Zero",fontsize=16,color="green",shape="box"];140[label="primPlusInt (Pos (Succ Zero)) (truncateM0 (Double vuy30 vuy31) (floatProperFractionDouble (Double vuy30 vuy31)))",fontsize=16,color="black",shape="box"];140 -> 151[label="",style="solid", color="black", weight=3];
141[label="primPlusInt (Pos (Succ Zero)) (truncateM0 vuy3 (truncateVu6 vuy3))",fontsize=16,color="black",shape="box"];141 -> 152[label="",style="solid", color="black", weight=3];
142[label="primPlusInt (Pos (Succ Zero)) (truncateM vuy3)",fontsize=16,color="black",shape="box"];142 -> 153[label="",style="solid", color="black", weight=3];
143[label="toEnum1 (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];143 -> 154[label="",style="solid", color="black", weight=3];
144[label="toEnum1 (Pos (Succ (Succ (primPlusNat Zero Zero))))",fontsize=16,color="black",shape="box"];144 -> 155[label="",style="solid", color="black", weight=3];
145[label="error []",fontsize=16,color="red",shape="box"];146[label="primPlusInt (Pos (Succ Zero)) (truncateM0 (Float vuy30 vuy31) (floatProperFractionFloat (Float vuy30 vuy31)))",fontsize=16,color="black",shape="box"];146 -> 156[label="",style="solid", color="black", weight=3];
147[label="toEnum9 (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];147 -> 157[label="",style="solid", color="black", weight=3];
148[label="toEnum9 (Pos (Succ (Succ (primPlusNat Zero Zero))))",fontsize=16,color="black",shape="box"];148 -> 158[label="",style="solid", color="black", weight=3];
149[label="toEnum9 (Pos (Succ (Succ (primPlusNat Zero (Succ Zero)))))",fontsize=16,color="black",shape="box"];149 -> 159[label="",style="solid", color="black", weight=3];
150[label="primPlusNat Zero vuy300",fontsize=16,color="burlywood",shape="triangle"];890[label="vuy300/Succ vuy3000",fontsize=10,color="white",style="solid",shape="box"];150 -> 890[label="",style="solid", color="burlywood", weight=9];
890 -> 160[label="",style="solid", color="burlywood", weight=3];
891[label="vuy300/Zero",fontsize=10,color="white",style="solid",shape="box"];150 -> 891[label="",style="solid", color="burlywood", weight=9];
891 -> 161[label="",style="solid", color="burlywood", weight=3];
151[label="primPlusInt (Pos (Succ Zero)) (truncateM0 (Double vuy30 vuy31) (fromInt (vuy30 `quot` vuy31),Double vuy30 vuy31 - fromInt (vuy30 `quot` vuy31)))",fontsize=16,color="black",shape="box"];151 -> 162[label="",style="solid", color="black", weight=3];
152[label="primPlusInt (Pos (Succ Zero)) (truncateM0 vuy3 (properFraction vuy3))",fontsize=16,color="burlywood",shape="box"];892[label="vuy3/vuy30 :% vuy31",fontsize=10,color="white",style="solid",shape="box"];152 -> 892[label="",style="solid", color="burlywood", weight=9];
892 -> 163[label="",style="solid", color="burlywood", weight=3];
153[label="primPlusInt (Pos (Succ Zero)) (truncateM0 vuy3 (truncateVu6 vuy3))",fontsize=16,color="black",shape="box"];153 -> 164[label="",style="solid", color="black", weight=3];
154[label="toEnum0 (Pos (Succ Zero) == Pos (Succ Zero)) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];154 -> 165[label="",style="solid", color="black", weight=3];
155 -> 166[label="",style="dashed", color="red", weight=0];
155[label="toEnum0 (Pos (Succ (Succ (primPlusNat Zero Zero))) == Pos (Succ Zero)) (Pos (Succ (Succ (primPlusNat Zero Zero))))",fontsize=16,color="magenta"];155 -> 167[label="",style="dashed", color="magenta", weight=3];
155 -> 168[label="",style="dashed", color="magenta", weight=3];
156[label="primPlusInt (Pos (Succ Zero)) (truncateM0 (Float vuy30 vuy31) (fromInt (vuy30 `quot` vuy31),Float vuy30 vuy31 - fromInt (vuy30 `quot` vuy31)))",fontsize=16,color="black",shape="box"];156 -> 169[label="",style="solid", color="black", weight=3];
157[label="toEnum8 (Pos (Succ Zero) == Pos (Succ Zero)) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];157 -> 170[label="",style="solid", color="black", weight=3];
158 -> 171[label="",style="dashed", color="red", weight=0];
158[label="toEnum8 (Pos (Succ (Succ (primPlusNat Zero Zero))) == Pos (Succ Zero)) (Pos (Succ (Succ (primPlusNat Zero Zero))))",fontsize=16,color="magenta"];158 -> 172[label="",style="dashed", color="magenta", weight=3];
158 -> 173[label="",style="dashed", color="magenta", weight=3];
159 -> 171[label="",style="dashed", color="red", weight=0];
159[label="toEnum8 (Pos (Succ (Succ (primPlusNat Zero (Succ Zero)))) == Pos (Succ Zero)) (Pos (Succ (Succ (primPlusNat Zero (Succ Zero)))))",fontsize=16,color="magenta"];159 -> 174[label="",style="dashed", color="magenta", weight=3];
159 -> 175[label="",style="dashed", color="magenta", weight=3];
160[label="primPlusNat Zero (Succ vuy3000)",fontsize=16,color="black",shape="box"];160 -> 176[label="",style="solid", color="black", weight=3];
161[label="primPlusNat Zero Zero",fontsize=16,color="black",shape="box"];161 -> 177[label="",style="solid", color="black", weight=3];
162[label="primPlusInt (Pos (Succ Zero)) (fromInt (vuy30 `quot` vuy31))",fontsize=16,color="black",shape="triangle"];162 -> 178[label="",style="solid", color="black", weight=3];
163[label="primPlusInt (Pos (Succ Zero)) (truncateM0 (vuy30 :% vuy31) (properFraction (vuy30 :% vuy31)))",fontsize=16,color="black",shape="box"];163 -> 179[label="",style="solid", color="black", weight=3];
164[label="primPlusInt (Pos (Succ Zero)) (truncateM0 vuy3 (properFraction vuy3))",fontsize=16,color="burlywood",shape="box"];896[label="vuy3/vuy30 :% vuy31",fontsize=10,color="white",style="solid",shape="box"];164 -> 896[label="",style="solid", color="burlywood", weight=9];
896 -> 180[label="",style="solid", color="burlywood", weight=3];
165[label="toEnum0 (primEqInt (Pos (Succ Zero)) (Pos (Succ Zero))) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];165 -> 181[label="",style="solid", color="black", weight=3];
167 -> 150[label="",style="dashed", color="red", weight=0];
167[label="primPlusNat Zero Zero",fontsize=16,color="magenta"];167 -> 182[label="",style="dashed", color="magenta", weight=3];
168 -> 150[label="",style="dashed", color="red", weight=0];
168[label="primPlusNat Zero Zero",fontsize=16,color="magenta"];168 -> 183[label="",style="dashed", color="magenta", weight=3];
166[label="toEnum0 (Pos (Succ (Succ vuy5)) == Pos (Succ Zero)) (Pos (Succ (Succ vuy4)))",fontsize=16,color="black",shape="triangle"];166 -> 184[label="",style="solid", color="black", weight=3];
169 -> 162[label="",style="dashed", color="red", weight=0];
169[label="primPlusInt (Pos (Succ Zero)) (fromInt (vuy30 `quot` vuy31))",fontsize=16,color="magenta"];169 -> 185[label="",style="dashed", color="magenta", weight=3];
169 -> 186[label="",style="dashed", color="magenta", weight=3];
170[label="toEnum8 (primEqInt (Pos (Succ Zero)) (Pos (Succ Zero))) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];170 -> 187[label="",style="solid", color="black", weight=3];
172 -> 150[label="",style="dashed", color="red", weight=0];
172[label="primPlusNat Zero Zero",fontsize=16,color="magenta"];172 -> 188[label="",style="dashed", color="magenta", weight=3];
173 -> 150[label="",style="dashed", color="red", weight=0];
173[label="primPlusNat Zero Zero",fontsize=16,color="magenta"];173 -> 189[label="",style="dashed", color="magenta", weight=3];
171[label="toEnum8 (Pos (Succ (Succ vuy7)) == Pos (Succ Zero)) (Pos (Succ (Succ vuy6)))",fontsize=16,color="black",shape="triangle"];171 -> 190[label="",style="solid", color="black", weight=3];
174 -> 150[label="",style="dashed", color="red", weight=0];
174[label="primPlusNat Zero (Succ Zero)",fontsize=16,color="magenta"];174 -> 191[label="",style="dashed", color="magenta", weight=3];
175 -> 150[label="",style="dashed", color="red", weight=0];
175[label="primPlusNat Zero (Succ Zero)",fontsize=16,color="magenta"];175 -> 192[label="",style="dashed", color="magenta", weight=3];
176[label="Succ vuy3000",fontsize=16,color="green",shape="box"];177[label="Zero",fontsize=16,color="green",shape="box"];178[label="primPlusInt (Pos (Succ Zero)) (vuy30 `quot` vuy31)",fontsize=16,color="black",shape="box"];178 -> 193[label="",style="solid", color="black", weight=3];
179[label="primPlusInt (Pos (Succ Zero)) (truncateM0 (vuy30 :% vuy31) (fromIntegral (properFractionQ vuy30 vuy31),properFractionR vuy30 vuy31 :% vuy31))",fontsize=16,color="black",shape="box"];179 -> 194[label="",style="solid", color="black", weight=3];
180[label="primPlusInt (Pos (Succ Zero)) (truncateM0 (vuy30 :% vuy31) (properFraction (vuy30 :% vuy31)))",fontsize=16,color="black",shape="box"];180 -> 195[label="",style="solid", color="black", weight=3];
181[label="toEnum0 (primEqNat Zero Zero) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];181 -> 196[label="",style="solid", color="black", weight=3];
182[label="Zero",fontsize=16,color="green",shape="box"];183[label="Zero",fontsize=16,color="green",shape="box"];184[label="toEnum0 (primEqInt (Pos (Succ (Succ vuy5))) (Pos (Succ Zero))) (Pos (Succ (Succ vuy4)))",fontsize=16,color="black",shape="box"];184 -> 197[label="",style="solid", color="black", weight=3];
185[label="vuy30",fontsize=16,color="green",shape="box"];186[label="vuy31",fontsize=16,color="green",shape="box"];187[label="toEnum8 (primEqNat Zero Zero) (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];187 -> 198[label="",style="solid", color="black", weight=3];
188[label="Zero",fontsize=16,color="green",shape="box"];189[label="Zero",fontsize=16,color="green",shape="box"];190[label="toEnum8 (primEqInt (Pos (Succ (Succ vuy7))) (Pos (Succ Zero))) (Pos (Succ (Succ vuy6)))",fontsize=16,color="black",shape="box"];190 -> 199[label="",style="solid", color="black", weight=3];
191[label="Succ Zero",fontsize=16,color="green",shape="box"];192[label="Succ Zero",fontsize=16,color="green",shape="box"];193[label="primPlusInt (Pos (Succ Zero)) (primQuotInt vuy30 vuy31)",fontsize=16,color="burlywood",shape="triangle"];904[label="vuy30/Pos vuy300",fontsize=10,color="white",style="solid",shape="box"];193 -> 904[label="",style="solid", color="burlywood", weight=9];
904 -> 200[label="",style="solid", color="burlywood", weight=3];
905[label="vuy30/Neg vuy300",fontsize=10,color="white",style="solid",shape="box"];193 -> 905[label="",style="solid", color="burlywood", weight=9];
905 -> 201[label="",style="solid", color="burlywood", weight=3];
194[label="primPlusInt (Pos (Succ Zero)) (fromIntegral (properFractionQ vuy30 vuy31))",fontsize=16,color="black",shape="box"];194 -> 202[label="",style="solid", color="black", weight=3];
195[label="primPlusInt (Pos (Succ Zero)) (truncateM0 (vuy30 :% vuy31) (fromIntegral (properFractionQ vuy30 vuy31),properFractionR vuy30 vuy31 :% vuy31))",fontsize=16,color="black",shape="box"];195 -> 203[label="",style="solid", color="black", weight=3];
196[label="toEnum0 True (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];196 -> 204[label="",style="solid", color="black", weight=3];
197[label="toEnum0 (primEqNat (Succ vuy5) Zero) (Pos (Succ (Succ vuy4)))",fontsize=16,color="black",shape="box"];197 -> 205[label="",style="solid", color="black", weight=3];
198[label="toEnum8 True (Pos (Succ Zero))",fontsize=16,color="black",shape="box"];198 -> 206[label="",style="solid", color="black", weight=3];
199[label="toEnum8 (primEqNat (Succ vuy7) Zero) (Pos (Succ (Succ vuy6)))",fontsize=16,color="black",shape="box"];199 -> 207[label="",style="solid", color="black", weight=3];
200[label="primPlusInt (Pos (Succ Zero)) (primQuotInt (Pos vuy300) vuy31)",fontsize=16,color="burlywood",shape="box"];906[label="vuy31/Pos vuy310",fontsize=10,color="white",style="solid",shape="box"];200 -> 906[label="",style="solid", color="burlywood", weight=9];
906 -> 208[label="",style="solid", color="burlywood", weight=3];
907[label="vuy31/Neg vuy310",fontsize=10,color="white",style="solid",shape="box"];200 -> 907[label="",style="solid", color="burlywood", weight=9];
907 -> 209[label="",style="solid", color="burlywood", weight=3];
201[label="primPlusInt (Pos (Succ Zero)) (primQuotInt (Neg vuy300) vuy31)",fontsize=16,color="burlywood",shape="box"];908[label="vuy31/Pos vuy310",fontsize=10,color="white",style="solid",shape="box"];201 -> 908[label="",style="solid", color="burlywood", weight=9];
908 -> 210[label="",style="solid", color="burlywood", weight=3];
909[label="vuy31/Neg vuy310",fontsize=10,color="white",style="solid",shape="box"];201 -> 909[label="",style="solid", color="burlywood", weight=9];
909 -> 211[label="",style="solid", color="burlywood", weight=3];
202[label="primPlusInt (Pos (Succ Zero)) (fromInteger . toInteger)",fontsize=16,color="black",shape="box"];202 -> 212[label="",style="solid", color="black", weight=3];
203[label="primPlusInt (Pos (Succ Zero)) (fromIntegral (properFractionQ vuy30 vuy31))",fontsize=16,color="black",shape="box"];203 -> 213[label="",style="solid", color="black", weight=3];
204[label="True",fontsize=16,color="green",shape="box"];205[label="toEnum0 False (Pos (Succ (Succ vuy4)))",fontsize=16,color="black",shape="box"];205 -> 214[label="",style="solid", color="black", weight=3];
206[label="EQ",fontsize=16,color="green",shape="box"];207[label="toEnum8 False (Pos (Succ (Succ vuy6)))",fontsize=16,color="black",shape="box"];207 -> 215[label="",style="solid", color="black", weight=3];
208[label="primPlusInt (Pos (Succ Zero)) (primQuotInt (Pos vuy300) (Pos vuy310))",fontsize=16,color="burlywood",shape="box"];910[label="vuy310/Succ vuy3100",fontsize=10,color="white",style="solid",shape="box"];208 -> 910[label="",style="solid", color="burlywood", weight=9];
910 -> 216[label="",style="solid", color="burlywood", weight=3];
911[label="vuy310/Zero",fontsize=10,color="white",style="solid",shape="box"];208 -> 911[label="",style="solid", color="burlywood", weight=9];
911 -> 217[label="",style="solid", color="burlywood", weight=3];
209[label="primPlusInt (Pos (Succ Zero)) (primQuotInt (Pos vuy300) (Neg vuy310))",fontsize=16,color="burlywood",shape="box"];912[label="vuy310/Succ vuy3100",fontsize=10,color="white",style="solid",shape="box"];209 -> 912[label="",style="solid", color="burlywood", weight=9];
912 -> 218[label="",style="solid", color="burlywood", weight=3];
913[label="vuy310/Zero",fontsize=10,color="white",style="solid",shape="box"];209 -> 913[label="",style="solid", color="burlywood", weight=9];
913 -> 219[label="",style="solid", color="burlywood", weight=3];
210[label="primPlusInt (Pos (Succ Zero)) (primQuotInt (Neg vuy300) (Pos vuy310))",fontsize=16,color="burlywood",shape="box"];914[label="vuy310/Succ vuy3100",fontsize=10,color="white",style="solid",shape="box"];210 -> 914[label="",style="solid", color="burlywood", weight=9];
914 -> 220[label="",style="solid", color="burlywood", weight=3];
915[label="vuy310/Zero",fontsize=10,color="white",style="solid",shape="box"];210 -> 915[label="",style="solid", color="burlywood", weight=9];
915 -> 221[label="",style="solid", color="burlywood", weight=3];
211[label="primPlusInt (Pos (Succ Zero)) (primQuotInt (Neg vuy300) (Neg vuy310))",fontsize=16,color="burlywood",shape="box"];916[label="vuy310/Succ vuy3100",fontsize=10,color="white",style="solid",shape="box"];211 -> 916[label="",style="solid", color="burlywood", weight=9];
916 -> 222[label="",style="solid", color="burlywood", weight=3];
917[label="vuy310/Zero",fontsize=10,color="white",style="solid",shape="box"];211 -> 917[label="",style="solid", color="burlywood", weight=9];
917 -> 223[label="",style="solid", color="burlywood", weight=3];
212[label="primPlusInt (Pos (Succ Zero)) (fromInteger (toInteger (properFractionQ vuy30 vuy31)))",fontsize=16,color="black",shape="box"];212 -> 224[label="",style="solid", color="black", weight=3];
213[label="primPlusInt (Pos (Succ Zero)) (fromInteger . toInteger)",fontsize=16,color="black",shape="box"];213 -> 225[label="",style="solid", color="black", weight=3];
214[label="error []",fontsize=16,color="red",shape="box"];215[label="toEnum7 (Pos (Succ (Succ vuy6)))",fontsize=16,color="black",shape="box"];215 -> 226[label="",style="solid", color="black", weight=3];
216[label="primPlusInt (Pos (Succ Zero)) (primQuotInt (Pos vuy300) (Pos (Succ vuy3100)))",fontsize=16,color="black",shape="box"];216 -> 227[label="",style="solid", color="black", weight=3];
217[label="primPlusInt (Pos (Succ Zero)) (primQuotInt (Pos vuy300) (Pos Zero))",fontsize=16,color="black",shape="box"];217 -> 228[label="",style="solid", color="black", weight=3];
218[label="primPlusInt (Pos (Succ Zero)) (primQuotInt (Pos vuy300) (Neg (Succ vuy3100)))",fontsize=16,color="black",shape="box"];218 -> 229[label="",style="solid", color="black", weight=3];
219[label="primPlusInt (Pos (Succ Zero)) (primQuotInt (Pos vuy300) (Neg Zero))",fontsize=16,color="black",shape="box"];219 -> 230[label="",style="solid", color="black", weight=3];
220[label="primPlusInt (Pos (Succ Zero)) (primQuotInt (Neg vuy300) (Pos (Succ vuy3100)))",fontsize=16,color="black",shape="box"];220 -> 231[label="",style="solid", color="black", weight=3];
221[label="primPlusInt (Pos (Succ Zero)) (primQuotInt (Neg vuy300) (Pos Zero))",fontsize=16,color="black",shape="box"];221 -> 232[label="",style="solid", color="black", weight=3];
222[label="primPlusInt (Pos (Succ Zero)) (primQuotInt (Neg vuy300) (Neg (Succ vuy3100)))",fontsize=16,color="black",shape="box"];222 -> 233[label="",style="solid", color="black", weight=3];
223[label="primPlusInt (Pos (Succ Zero)) (primQuotInt (Neg vuy300) (Neg Zero))",fontsize=16,color="black",shape="box"];223 -> 234[label="",style="solid", color="black", weight=3];
224[label="primPlusInt (Pos (Succ Zero)) (fromInteger (Integer (properFractionQ vuy30 vuy31)))",fontsize=16,color="black",shape="box"];224 -> 235[label="",style="solid", color="black", weight=3];
225[label="primPlusInt (Pos (Succ Zero)) (fromInteger (toInteger (properFractionQ vuy30 vuy31)))",fontsize=16,color="black",shape="box"];225 -> 236[label="",style="solid", color="black", weight=3];
226[label="toEnum6 (Pos (Succ (Succ vuy6)) == Pos (Succ (Succ Zero))) (Pos (Succ (Succ vuy6)))",fontsize=16,color="black",shape="box"];226 -> 237[label="",style="solid", color="black", weight=3];
227[label="primPlusInt (Pos (Succ Zero)) (Pos (primDivNatS vuy300 (Succ vuy3100)))",fontsize=16,color="black",shape="triangle"];227 -> 238[label="",style="solid", color="black", weight=3];
228[label="primPlusInt (Pos (Succ Zero)) (error [])",fontsize=16,color="black",shape="triangle"];228 -> 239[label="",style="solid", color="black", weight=3];
229[label="primPlusInt (Pos (Succ Zero)) (Neg (primDivNatS vuy300 (Succ vuy3100)))",fontsize=16,color="black",shape="triangle"];229 -> 240[label="",style="solid", color="black", weight=3];
230 -> 228[label="",style="dashed", color="red", weight=0];
230[label="primPlusInt (Pos (Succ Zero)) (error [])",fontsize=16,color="magenta"];231 -> 229[label="",style="dashed", color="red", weight=0];
231[label="primPlusInt (Pos (Succ Zero)) (Neg (primDivNatS vuy300 (Succ vuy3100)))",fontsize=16,color="magenta"];231 -> 241[label="",style="dashed", color="magenta", weight=3];
231 -> 242[label="",style="dashed", color="magenta", weight=3];
232 -> 228[label="",style="dashed", color="red", weight=0];
232[label="primPlusInt (Pos (Succ Zero)) (error [])",fontsize=16,color="magenta"];233 -> 227[label="",style="dashed", color="red", weight=0];
233[label="primPlusInt (Pos (Succ Zero)) (Pos (primDivNatS vuy300 (Succ vuy3100)))",fontsize=16,color="magenta"];233 -> 243[label="",style="dashed", color="magenta", weight=3];
233 -> 244[label="",style="dashed", color="magenta", weight=3];
234 -> 228[label="",style="dashed", color="red", weight=0];
234[label="primPlusInt (Pos (Succ Zero)) (error [])",fontsize=16,color="magenta"];235[label="primPlusInt (Pos (Succ Zero)) (properFractionQ vuy30 vuy31)",fontsize=16,color="black",shape="box"];235 -> 245[label="",style="solid", color="black", weight=3];
236[label="primPlusInt (Pos (Succ Zero)) (fromInteger (properFractionQ vuy30 vuy31))",fontsize=16,color="black",shape="box"];236 -> 246[label="",style="solid", color="black", weight=3];
237[label="toEnum6 (primEqInt (Pos (Succ (Succ vuy6))) (Pos (Succ (Succ Zero)))) (Pos (Succ (Succ vuy6)))",fontsize=16,color="black",shape="box"];237 -> 247[label="",style="solid", color="black", weight=3];
238[label="Pos (primPlusNat (Succ Zero) (primDivNatS vuy300 (Succ vuy3100)))",fontsize=16,color="green",shape="box"];238 -> 248[label="",style="dashed", color="green", weight=3];
239[label="error []",fontsize=16,color="red",shape="box"];240[label="primMinusNat (Succ Zero) (primDivNatS vuy300 (Succ vuy3100))",fontsize=16,color="burlywood",shape="box"];923[label="vuy300/Succ vuy3000",fontsize=10,color="white",style="solid",shape="box"];240 -> 923[label="",style="solid", color="burlywood", weight=9];
923 -> 249[label="",style="solid", color="burlywood", weight=3];
924[label="vuy300/Zero",fontsize=10,color="white",style="solid",shape="box"];240 -> 924[label="",style="solid", color="burlywood", weight=9];
924 -> 250[label="",style="solid", color="burlywood", weight=3];
241[label="vuy3100",fontsize=16,color="green",shape="box"];242[label="vuy300",fontsize=16,color="green",shape="box"];243[label="vuy300",fontsize=16,color="green",shape="box"];244[label="vuy3100",fontsize=16,color="green",shape="box"];245[label="primPlusInt (Pos (Succ Zero)) (properFractionQ1 vuy30 vuy31 (properFractionVu30 vuy30 vuy31))",fontsize=16,color="black",shape="box"];245 -> 251[label="",style="solid", color="black", weight=3];
246[label="primPlusInt (Pos (Succ Zero)) (fromInteger (properFractionQ1 vuy30 vuy31 (properFractionVu30 vuy30 vuy31)))",fontsize=16,color="black",shape="box"];246 -> 252[label="",style="solid", color="black", weight=3];
247[label="toEnum6 (primEqNat (Succ vuy6) (Succ Zero)) (Pos (Succ (Succ vuy6)))",fontsize=16,color="black",shape="box"];247 -> 253[label="",style="solid", color="black", weight=3];
248 -> 115[label="",style="dashed", color="red", weight=0];
248[label="primPlusNat (Succ Zero) (primDivNatS vuy300 (Succ vuy3100))",fontsize=16,color="magenta"];248 -> 254[label="",style="dashed", color="magenta", weight=3];
249[label="primMinusNat (Succ Zero) (primDivNatS (Succ vuy3000) (Succ vuy3100))",fontsize=16,color="black",shape="box"];249 -> 255[label="",style="solid", color="black", weight=3];
250[label="primMinusNat (Succ Zero) (primDivNatS Zero (Succ vuy3100))",fontsize=16,color="black",shape="box"];250 -> 256[label="",style="solid", color="black", weight=3];
251[label="primPlusInt (Pos (Succ Zero)) (properFractionQ1 vuy30 vuy31 (quotRem vuy30 vuy31))",fontsize=16,color="black",shape="box"];251 -> 257[label="",style="solid", color="black", weight=3];
252[label="primPlusInt (Pos (Succ Zero)) (fromInteger (properFractionQ1 vuy30 vuy31 (quotRem vuy30 vuy31)))",fontsize=16,color="burlywood",shape="box"];926[label="vuy30/Integer vuy300",fontsize=10,color="white",style="solid",shape="box"];252 -> 926[label="",style="solid", color="burlywood", weight=9];
926 -> 258[label="",style="solid", color="burlywood", weight=3];
253[label="toEnum6 (primEqNat vuy6 Zero) (Pos (Succ (Succ vuy6)))",fontsize=16,color="burlywood",shape="box"];927[label="vuy6/Succ vuy60",fontsize=10,color="white",style="solid",shape="box"];253 -> 927[label="",style="solid", color="burlywood", weight=9];
927 -> 259[label="",style="solid", color="burlywood", weight=3];
928[label="vuy6/Zero",fontsize=10,color="white",style="solid",shape="box"];253 -> 928[label="",style="solid", color="burlywood", weight=9];
928 -> 260[label="",style="solid", color="burlywood", weight=3];
254[label="primDivNatS vuy300 (Succ vuy3100)",fontsize=16,color="burlywood",shape="triangle"];929[label="vuy300/Succ vuy3000",fontsize=10,color="white",style="solid",shape="box"];254 -> 929[label="",style="solid", color="burlywood", weight=9];
929 -> 261[label="",style="solid", color="burlywood", weight=3];
930[label="vuy300/Zero",fontsize=10,color="white",style="solid",shape="box"];254 -> 930[label="",style="solid", color="burlywood", weight=9];
930 -> 262[label="",style="solid", color="burlywood", weight=3];
255[label="primMinusNat (Succ Zero) (primDivNatS0 vuy3000 vuy3100 (primGEqNatS vuy3000 vuy3100))",fontsize=16,color="burlywood",shape="box"];931[label="vuy3000/Succ vuy30000",fontsize=10,color="white",style="solid",shape="box"];255 -> 931[label="",style="solid", color="burlywood", weight=9];
931 -> 263[label="",style="solid", color="burlywood", weight=3];
932[label="vuy3000/Zero",fontsize=10,color="white",style="solid",shape="box"];255 -> 932[label="",style="solid", color="burlywood", weight=9];
932 -> 264[label="",style="solid", color="burlywood", weight=3];
256[label="primMinusNat (Succ Zero) Zero",fontsize=16,color="black",shape="triangle"];256 -> 265[label="",style="solid", color="black", weight=3];
257[label="primPlusInt (Pos (Succ Zero)) (properFractionQ1 vuy30 vuy31 (primQrmInt vuy30 vuy31))",fontsize=16,color="black",shape="box"];257 -> 266[label="",style="solid", color="black", weight=3];
258[label="primPlusInt (Pos (Succ Zero)) (fromInteger (properFractionQ1 (Integer vuy300) vuy31 (quotRem (Integer vuy300) vuy31)))",fontsize=16,color="burlywood",shape="box"];933[label="vuy31/Integer vuy310",fontsize=10,color="white",style="solid",shape="box"];258 -> 933[label="",style="solid", color="burlywood", weight=9];
933 -> 267[label="",style="solid", color="burlywood", weight=3];
259[label="toEnum6 (primEqNat (Succ vuy60) Zero) (Pos (Succ (Succ (Succ vuy60))))",fontsize=16,color="black",shape="box"];259 -> 268[label="",style="solid", color="black", weight=3];
260[label="toEnum6 (primEqNat Zero Zero) (Pos (Succ (Succ Zero)))",fontsize=16,color="black",shape="box"];260 -> 269[label="",style="solid", color="black", weight=3];
261[label="primDivNatS (Succ vuy3000) (Succ vuy3100)",fontsize=16,color="black",shape="box"];261 -> 270[label="",style="solid", color="black", weight=3];
262[label="primDivNatS Zero (Succ vuy3100)",fontsize=16,color="black",shape="box"];262 -> 271[label="",style="solid", color="black", weight=3];
263[label="primMinusNat (Succ Zero) (primDivNatS0 (Succ vuy30000) vuy3100 (primGEqNatS (Succ vuy30000) vuy3100))",fontsize=16,color="burlywood",shape="box"];934[label="vuy3100/Succ vuy31000",fontsize=10,color="white",style="solid",shape="box"];263 -> 934[label="",style="solid", color="burlywood", weight=9];
934 -> 272[label="",style="solid", color="burlywood", weight=3];
935[label="vuy3100/Zero",fontsize=10,color="white",style="solid",shape="box"];263 -> 935[label="",style="solid", color="burlywood", weight=9];
935 -> 273[label="",style="solid", color="burlywood", weight=3];
264[label="primMinusNat (Succ Zero) (primDivNatS0 Zero vuy3100 (primGEqNatS Zero vuy3100))",fontsize=16,color="burlywood",shape="box"];936[label="vuy3100/Succ vuy31000",fontsize=10,color="white",style="solid",shape="box"];264 -> 936[label="",style="solid", color="burlywood", weight=9];
936 -> 274[label="",style="solid", color="burlywood", weight=3];
937[label="vuy3100/Zero",fontsize=10,color="white",style="solid",shape="box"];264 -> 937[label="",style="solid", color="burlywood", weight=9];
937 -> 275[label="",style="solid", color="burlywood", weight=3];
265[label="Pos (Succ Zero)",fontsize=16,color="green",shape="box"];266[label="primPlusInt (Pos (Succ Zero)) (properFractionQ1 vuy30 vuy31 (primQuotInt vuy30 vuy31,primRemInt vuy30 vuy31))",fontsize=16,color="black",shape="box"];266 -> 276[label="",style="solid", color="black", weight=3];
267[label="primPlusInt (Pos (Succ Zero)) (fromInteger (properFractionQ1 (Integer vuy300) (Integer vuy310) (quotRem (Integer vuy300) (Integer vuy310))))",fontsize=16,color="black",shape="box"];267 -> 277[label="",style="solid", color="black", weight=3];
268[label="toEnum6 False (Pos (Succ (Succ (Succ vuy60))))",fontsize=16,color="black",shape="box"];268 -> 278[label="",style="solid", color="black", weight=3];
269[label="toEnum6 True (Pos (Succ (Succ Zero)))",fontsize=16,color="black",shape="box"];269 -> 279[label="",style="solid", color="black", weight=3];
270[label="primDivNatS0 vuy3000 vuy3100 (primGEqNatS vuy3000 vuy3100)",fontsize=16,color="burlywood",shape="box"];938[label="vuy3000/Succ vuy30000",fontsize=10,color="white",style="solid",shape="box"];270 -> 938[label="",style="solid", color="burlywood", weight=9];
938 -> 280[label="",style="solid", color="burlywood", weight=3];
939[label="vuy3000/Zero",fontsize=10,color="white",style="solid",shape="box"];270 -> 939[label="",style="solid", color="burlywood", weight=9];
939 -> 281[label="",style="solid", color="burlywood", weight=3];
271[label="Zero",fontsize=16,color="green",shape="box"];272[label="primMinusNat (Succ Zero) (primDivNatS0 (Succ vuy30000) (Succ vuy31000) (primGEqNatS (Succ vuy30000) (Succ vuy31000)))",fontsize=16,color="black",shape="box"];272 -> 282[label="",style="solid", color="black", weight=3];
273[label="primMinusNat (Succ Zero) (primDivNatS0 (Succ vuy30000) Zero (primGEqNatS (Succ vuy30000) Zero))",fontsize=16,color="black",shape="box"];273 -> 283[label="",style="solid", color="black", weight=3];
274[label="primMinusNat (Succ Zero) (primDivNatS0 Zero (Succ vuy31000) (primGEqNatS Zero (Succ vuy31000)))",fontsize=16,color="black",shape="box"];274 -> 284[label="",style="solid", color="black", weight=3];
275[label="primMinusNat (Succ Zero) (primDivNatS0 Zero Zero (primGEqNatS Zero Zero))",fontsize=16,color="black",shape="box"];275 -> 285[label="",style="solid", color="black", weight=3];
276 -> 193[label="",style="dashed", color="red", weight=0];
276[label="primPlusInt (Pos (Succ Zero)) (primQuotInt vuy30 vuy31)",fontsize=16,color="magenta"];276 -> 286[label="",style="dashed", color="magenta", weight=3];
276 -> 287[label="",style="dashed", color="magenta", weight=3];
277[label="primPlusInt (Pos (Succ Zero)) (fromInteger (properFractionQ1 (Integer vuy300) (Integer vuy310) (Integer (primQuotInt vuy300 vuy310),Integer (primRemInt vuy300 vuy310))))",fontsize=16,color="black",shape="box"];277 -> 288[label="",style="solid", color="black", weight=3];
278[label="error []",fontsize=16,color="red",shape="box"];279[label="GT",fontsize=16,color="green",shape="box"];280[label="primDivNatS0 (Succ vuy30000) vuy3100 (primGEqNatS (Succ vuy30000) vuy3100)",fontsize=16,color="burlywood",shape="box"];941[label="vuy3100/Succ vuy31000",fontsize=10,color="white",style="solid",shape="box"];280 -> 941[label="",style="solid", color="burlywood", weight=9];
941 -> 289[label="",style="solid", color="burlywood", weight=3];
942[label="vuy3100/Zero",fontsize=10,color="white",style="solid",shape="box"];280 -> 942[label="",style="solid", color="burlywood", weight=9];
942 -> 290[label="",style="solid", color="burlywood", weight=3];
281[label="primDivNatS0 Zero vuy3100 (primGEqNatS Zero vuy3100)",fontsize=16,color="burlywood",shape="box"];943[label="vuy3100/Succ vuy31000",fontsize=10,color="white",style="solid",shape="box"];281 -> 943[label="",style="solid", color="burlywood", weight=9];
943 -> 291[label="",style="solid", color="burlywood", weight=3];
944[label="vuy3100/Zero",fontsize=10,color="white",style="solid",shape="box"];281 -> 944[label="",style="solid", color="burlywood", weight=9];
944 -> 292[label="",style="solid", color="burlywood", weight=3];
282 -> 716[label="",style="dashed", color="red", weight=0];
282[label="primMinusNat (Succ Zero) (primDivNatS0 (Succ vuy30000) (Succ vuy31000) (primGEqNatS vuy30000 vuy31000))",fontsize=16,color="magenta"];282 -> 717[label="",style="dashed", color="magenta", weight=3];
282 -> 718[label="",style="dashed", color="magenta", weight=3];
282 -> 719[label="",style="dashed", color="magenta", weight=3];
282 -> 720[label="",style="dashed", color="magenta", weight=3];
283[label="primMinusNat (Succ Zero) (primDivNatS0 (Succ vuy30000) Zero True)",fontsize=16,color="black",shape="box"];283 -> 295[label="",style="solid", color="black", weight=3];
284[label="primMinusNat (Succ Zero) (primDivNatS0 Zero (Succ vuy31000) False)",fontsize=16,color="black",shape="box"];284 -> 296[label="",style="solid", color="black", weight=3];
285[label="primMinusNat (Succ Zero) (primDivNatS0 Zero Zero True)",fontsize=16,color="black",shape="box"];285 -> 297[label="",style="solid", color="black", weight=3];
286[label="vuy30",fontsize=16,color="green",shape="box"];287[label="vuy31",fontsize=16,color="green",shape="box"];288[label="primPlusInt (Pos (Succ Zero)) (fromInteger (Integer (primQuotInt vuy300 vuy310)))",fontsize=16,color="black",shape="box"];288 -> 298[label="",style="solid", color="black", weight=3];
289[label="primDivNatS0 (Succ vuy30000) (Succ vuy31000) (primGEqNatS (Succ vuy30000) (Succ vuy31000))",fontsize=16,color="black",shape="box"];289 -> 299[label="",style="solid", color="black", weight=3];
290[label="primDivNatS0 (Succ vuy30000) Zero (primGEqNatS (Succ vuy30000) Zero)",fontsize=16,color="black",shape="box"];290 -> 300[label="",style="solid", color="black", weight=3];
291[label="primDivNatS0 Zero (Succ vuy31000) (primGEqNatS Zero (Succ vuy31000))",fontsize=16,color="black",shape="box"];291 -> 301[label="",style="solid", color="black", weight=3];
292[label="primDivNatS0 Zero Zero (primGEqNatS Zero Zero)",fontsize=16,color="black",shape="box"];292 -> 302[label="",style="solid", color="black", weight=3];
717[label="vuy31000",fontsize=16,color="green",shape="box"];718[label="vuy30000",fontsize=16,color="green",shape="box"];719[label="vuy31000",fontsize=16,color="green",shape="box"];720[label="vuy30000",fontsize=16,color="green",shape="box"];716[label="primMinusNat (Succ Zero) (primDivNatS0 (Succ vuy39) (Succ vuy40) (primGEqNatS vuy41 vuy42))",fontsize=16,color="burlywood",shape="triangle"];946[label="vuy41/Succ vuy410",fontsize=10,color="white",style="solid",shape="box"];716 -> 946[label="",style="solid", color="burlywood", weight=9];
946 -> 757[label="",style="solid", color="burlywood", weight=3];
947[label="vuy41/Zero",fontsize=10,color="white",style="solid",shape="box"];716 -> 947[label="",style="solid", color="burlywood", weight=9];
947 -> 758[label="",style="solid", color="burlywood", weight=3];
295 -> 307[label="",style="dashed", color="red", weight=0];
295[label="primMinusNat (Succ Zero) (Succ (primDivNatS (primMinusNatS (Succ vuy30000) Zero) (Succ Zero)))",fontsize=16,color="magenta"];295 -> 308[label="",style="dashed", color="magenta", weight=3];
296 -> 256[label="",style="dashed", color="red", weight=0];
296[label="primMinusNat (Succ Zero) Zero",fontsize=16,color="magenta"];297 -> 307[label="",style="dashed", color="red", weight=0];
297[label="primMinusNat (Succ Zero) (Succ (primDivNatS (primMinusNatS Zero Zero) (Succ Zero)))",fontsize=16,color="magenta"];297 -> 309[label="",style="dashed", color="magenta", weight=3];
298 -> 193[label="",style="dashed", color="red", weight=0];
298[label="primPlusInt (Pos (Succ Zero)) (primQuotInt vuy300 vuy310)",fontsize=16,color="magenta"];298 -> 310[label="",style="dashed", color="magenta", weight=3];
298 -> 311[label="",style="dashed", color="magenta", weight=3];
299 -> 782[label="",style="dashed", color="red", weight=0];
299[label="primDivNatS0 (Succ vuy30000) (Succ vuy31000) (primGEqNatS vuy30000 vuy31000)",fontsize=16,color="magenta"];299 -> 783[label="",style="dashed", color="magenta", weight=3];
299 -> 784[label="",style="dashed", color="magenta", weight=3];
299 -> 785[label="",style="dashed", color="magenta", weight=3];
299 -> 786[label="",style="dashed", color="magenta", weight=3];
300[label="primDivNatS0 (Succ vuy30000) Zero True",fontsize=16,color="black",shape="box"];300 -> 314[label="",style="solid", color="black", weight=3];
301[label="primDivNatS0 Zero (Succ vuy31000) False",fontsize=16,color="black",shape="box"];301 -> 315[label="",style="solid", color="black", weight=3];
302[label="primDivNatS0 Zero Zero True",fontsize=16,color="black",shape="box"];302 -> 316[label="",style="solid", color="black", weight=3];
757[label="primMinusNat (Succ Zero) (primDivNatS0 (Succ vuy39) (Succ vuy40) (primGEqNatS (Succ vuy410) vuy42))",fontsize=16,color="burlywood",shape="box"];953[label="vuy42/Succ vuy420",fontsize=10,color="white",style="solid",shape="box"];757 -> 953[label="",style="solid", color="burlywood", weight=9];
953 -> 763[label="",style="solid", color="burlywood", weight=3];
954[label="vuy42/Zero",fontsize=10,color="white",style="solid",shape="box"];757 -> 954[label="",style="solid", color="burlywood", weight=9];
954 -> 764[label="",style="solid", color="burlywood", weight=3];
758[label="primMinusNat (Succ Zero) (primDivNatS0 (Succ vuy39) (Succ vuy40) (primGEqNatS Zero vuy42))",fontsize=16,color="burlywood",shape="box"];955[label="vuy42/Succ vuy420",fontsize=10,color="white",style="solid",shape="box"];758 -> 955[label="",style="solid", color="burlywood", weight=9];
955 -> 765[label="",style="solid", color="burlywood", weight=3];
956[label="vuy42/Zero",fontsize=10,color="white",style="solid",shape="box"];758 -> 956[label="",style="solid", color="burlywood", weight=9];
956 -> 766[label="",style="solid", color="burlywood", weight=3];
308 -> 254[label="",style="dashed", color="red", weight=0];
308[label="primDivNatS (primMinusNatS (Succ vuy30000) Zero) (Succ Zero)",fontsize=16,color="magenta"];308 -> 321[label="",style="dashed", color="magenta", weight=3];
308 -> 322[label="",style="dashed", color="magenta", weight=3];
307[label="primMinusNat (Succ Zero) (Succ vuy8)",fontsize=16,color="black",shape="triangle"];307 -> 323[label="",style="solid", color="black", weight=3];
309 -> 254[label="",style="dashed", color="red", weight=0];
309[label="primDivNatS (primMinusNatS Zero Zero) (Succ Zero)",fontsize=16,color="magenta"];309 -> 324[label="",style="dashed", color="magenta", weight=3];
309 -> 325[label="",style="dashed", color="magenta", weight=3];
310[label="vuy300",fontsize=16,color="green",shape="box"];311[label="vuy310",fontsize=16,color="green",shape="box"];783[label="vuy31000",fontsize=16,color="green",shape="box"];784[label="vuy31000",fontsize=16,color="green",shape="box"];785[label="vuy30000",fontsize=16,color="green",shape="box"];786[label="vuy30000",fontsize=16,color="green",shape="box"];782[label="primDivNatS0 (Succ vuy52) (Succ vuy53) (primGEqNatS vuy54 vuy55)",fontsize=16,color="burlywood",shape="triangle"];959[label="vuy54/Succ vuy540",fontsize=10,color="white",style="solid",shape="box"];782 -> 959[label="",style="solid", color="burlywood", weight=9];
959 -> 823[label="",style="solid", color="burlywood", weight=3];
960[label="vuy54/Zero",fontsize=10,color="white",style="solid",shape="box"];782 -> 960[label="",style="solid", color="burlywood", weight=9];
960 -> 824[label="",style="solid", color="burlywood", weight=3];
314[label="Succ (primDivNatS (primMinusNatS (Succ vuy30000) Zero) (Succ Zero))",fontsize=16,color="green",shape="box"];314 -> 330[label="",style="dashed", color="green", weight=3];
315[label="Zero",fontsize=16,color="green",shape="box"];316[label="Succ (primDivNatS (primMinusNatS Zero Zero) (Succ Zero))",fontsize=16,color="green",shape="box"];316 -> 331[label="",style="dashed", color="green", weight=3];
763[label="primMinusNat (Succ Zero) (primDivNatS0 (Succ vuy39) (Succ vuy40) (primGEqNatS (Succ vuy410) (Succ vuy420)))",fontsize=16,color="black",shape="box"];763 -> 770[label="",style="solid", color="black", weight=3];
764[label="primMinusNat (Succ Zero) (primDivNatS0 (Succ vuy39) (Succ vuy40) (primGEqNatS (Succ vuy410) Zero))",fontsize=16,color="black",shape="box"];764 -> 771[label="",style="solid", color="black", weight=3];
765[label="primMinusNat (Succ Zero) (primDivNatS0 (Succ vuy39) (Succ vuy40) (primGEqNatS Zero (Succ vuy420)))",fontsize=16,color="black",shape="box"];765 -> 772[label="",style="solid", color="black", weight=3];
766[label="primMinusNat (Succ Zero) (primDivNatS0 (Succ vuy39) (Succ vuy40) (primGEqNatS Zero Zero))",fontsize=16,color="black",shape="box"];766 -> 773[label="",style="solid", color="black", weight=3];
321[label="primMinusNatS (Succ vuy30000) Zero",fontsize=16,color="black",shape="triangle"];321 -> 337[label="",style="solid", color="black", weight=3];
322[label="Zero",fontsize=16,color="green",shape="box"];323[label="primMinusNat Zero vuy8",fontsize=16,color="burlywood",shape="box"];961[label="vuy8/Succ vuy80",fontsize=10,color="white",style="solid",shape="box"];323 -> 961[label="",style="solid", color="burlywood", weight=9];
961 -> 338[label="",style="solid", color="burlywood", weight=3];
962[label="vuy8/Zero",fontsize=10,color="white",style="solid",shape="box"];323 -> 962[label="",style="solid", color="burlywood", weight=9];
962 -> 339[label="",style="solid", color="burlywood", weight=3];
324[label="primMinusNatS Zero Zero",fontsize=16,color="black",shape="triangle"];324 -> 340[label="",style="solid", color="black", weight=3];
325[label="Zero",fontsize=16,color="green",shape="box"];823[label="primDivNatS0 (Succ vuy52) (Succ vuy53) (primGEqNatS (Succ vuy540) vuy55)",fontsize=16,color="burlywood",shape="box"];963[label="vuy55/Succ vuy550",fontsize=10,color="white",style="solid",shape="box"];823 -> 963[label="",style="solid", color="burlywood", weight=9];
963 -> 826[label="",style="solid", color="burlywood", weight=3];
964[label="vuy55/Zero",fontsize=10,color="white",style="solid",shape="box"];823 -> 964[label="",style="solid", color="burlywood", weight=9];
964 -> 827[label="",style="solid", color="burlywood", weight=3];
824[label="primDivNatS0 (Succ vuy52) (Succ vuy53) (primGEqNatS Zero vuy55)",fontsize=16,color="burlywood",shape="box"];965[label="vuy55/Succ vuy550",fontsize=10,color="white",style="solid",shape="box"];824 -> 965[label="",style="solid", color="burlywood", weight=9];
965 -> 828[label="",style="solid", color="burlywood", weight=3];
966[label="vuy55/Zero",fontsize=10,color="white",style="solid",shape="box"];824 -> 966[label="",style="solid", color="burlywood", weight=9];
966 -> 829[label="",style="solid", color="burlywood", weight=3];
330 -> 254[label="",style="dashed", color="red", weight=0];
330[label="primDivNatS (primMinusNatS (Succ vuy30000) Zero) (Succ Zero)",fontsize=16,color="magenta"];330 -> 345[label="",style="dashed", color="magenta", weight=3];
330 -> 346[label="",style="dashed", color="magenta", weight=3];
331 -> 254[label="",style="dashed", color="red", weight=0];
331[label="primDivNatS (primMinusNatS Zero Zero) (Succ Zero)",fontsize=16,color="magenta"];331 -> 347[label="",style="dashed", color="magenta", weight=3];
331 -> 348[label="",style="dashed", color="magenta", weight=3];
770 -> 716[label="",style="dashed", color="red", weight=0];
770[label="primMinusNat (Succ Zero) (primDivNatS0 (Succ vuy39) (Succ vuy40) (primGEqNatS vuy410 vuy420))",fontsize=16,color="magenta"];770 -> 776[label="",style="dashed", color="magenta", weight=3];
770 -> 777[label="",style="dashed", color="magenta", weight=3];
771[label="primMinusNat (Succ Zero) (primDivNatS0 (Succ vuy39) (Succ vuy40) True)",fontsize=16,color="black",shape="triangle"];771 -> 778[label="",style="solid", color="black", weight=3];
772[label="primMinusNat (Succ Zero) (primDivNatS0 (Succ vuy39) (Succ vuy40) False)",fontsize=16,color="black",shape="box"];772 -> 779[label="",style="solid", color="black", weight=3];
773 -> 771[label="",style="dashed", color="red", weight=0];
773[label="primMinusNat (Succ Zero) (primDivNatS0 (Succ vuy39) (Succ vuy40) True)",fontsize=16,color="magenta"];337[label="Succ vuy30000",fontsize=16,color="green",shape="box"];338[label="primMinusNat Zero (Succ vuy80)",fontsize=16,color="black",shape="box"];338 -> 355[label="",style="solid", color="black", weight=3];
339[label="primMinusNat Zero Zero",fontsize=16,color="black",shape="box"];339 -> 356[label="",style="solid", color="black", weight=3];
340[label="Zero",fontsize=16,color="green",shape="box"];826[label="primDivNatS0 (Succ vuy52) (Succ vuy53) (primGEqNatS (Succ vuy540) (Succ vuy550))",fontsize=16,color="black",shape="box"];826 -> 832[label="",style="solid", color="black", weight=3];
827[label="primDivNatS0 (Succ vuy52) (Succ vuy53) (primGEqNatS (Succ vuy540) Zero)",fontsize=16,color="black",shape="box"];827 -> 833[label="",style="solid", color="black", weight=3];
828[label="primDivNatS0 (Succ vuy52) (Succ vuy53) (primGEqNatS Zero (Succ vuy550))",fontsize=16,color="black",shape="box"];828 -> 834[label="",style="solid", color="black", weight=3];
829[label="primDivNatS0 (Succ vuy52) (Succ vuy53) (primGEqNatS Zero Zero)",fontsize=16,color="black",shape="box"];829 -> 835[label="",style="solid", color="black", weight=3];
345 -> 321[label="",style="dashed", color="red", weight=0];
345[label="primMinusNatS (Succ vuy30000) Zero",fontsize=16,color="magenta"];346[label="Zero",fontsize=16,color="green",shape="box"];347 -> 324[label="",style="dashed", color="red", weight=0];
347[label="primMinusNatS Zero Zero",fontsize=16,color="magenta"];348[label="Zero",fontsize=16,color="green",shape="box"];776[label="vuy420",fontsize=16,color="green",shape="box"];777[label="vuy410",fontsize=16,color="green",shape="box"];778 -> 307[label="",style="dashed", color="red", weight=0];
778[label="primMinusNat (Succ Zero) (Succ (primDivNatS (primMinusNatS (Succ vuy39) (Succ vuy40)) (Succ (Succ vuy40))))",fontsize=16,color="magenta"];778 -> 825[label="",style="dashed", color="magenta", weight=3];
779 -> 256[label="",style="dashed", color="red", weight=0];
779[label="primMinusNat (Succ Zero) Zero",fontsize=16,color="magenta"];355[label="Neg (Succ vuy80)",fontsize=16,color="green",shape="box"];356[label="Pos Zero",fontsize=16,color="green",shape="box"];832 -> 782[label="",style="dashed", color="red", weight=0];
832[label="primDivNatS0 (Succ vuy52) (Succ vuy53) (primGEqNatS vuy540 vuy550)",fontsize=16,color="magenta"];832 -> 837[label="",style="dashed", color="magenta", weight=3];
832 -> 838[label="",style="dashed", color="magenta", weight=3];
833[label="primDivNatS0 (Succ vuy52) (Succ vuy53) True",fontsize=16,color="black",shape="triangle"];833 -> 839[label="",style="solid", color="black", weight=3];
834[label="primDivNatS0 (Succ vuy52) (Succ vuy53) False",fontsize=16,color="black",shape="box"];834 -> 840[label="",style="solid", color="black", weight=3];
835 -> 833[label="",style="dashed", color="red", weight=0];
835[label="primDivNatS0 (Succ vuy52) (Succ vuy53) True",fontsize=16,color="magenta"];825 -> 254[label="",style="dashed", color="red", weight=0];
825[label="primDivNatS (primMinusNatS (Succ vuy39) (Succ vuy40)) (Succ (Succ vuy40))",fontsize=16,color="magenta"];825 -> 830[label="",style="dashed", color="magenta", weight=3];
825 -> 831[label="",style="dashed", color="magenta", weight=3];
837[label="vuy550",fontsize=16,color="green",shape="box"];838[label="vuy540",fontsize=16,color="green",shape="box"];839[label="Succ (primDivNatS (primMinusNatS (Succ vuy52) (Succ vuy53)) (Succ (Succ vuy53)))",fontsize=16,color="green",shape="box"];839 -> 843[label="",style="dashed", color="green", weight=3];
840[label="Zero",fontsize=16,color="green",shape="box"];830[label="primMinusNatS (Succ vuy39) (Succ vuy40)",fontsize=16,color="black",shape="box"];830 -> 836[label="",style="solid", color="black", weight=3];
831[label="Succ vuy40",fontsize=16,color="green",shape="box"];843 -> 254[label="",style="dashed", color="red", weight=0];
843[label="primDivNatS (primMinusNatS (Succ vuy52) (Succ vuy53)) (Succ (Succ vuy53))",fontsize=16,color="magenta"];843 -> 848[label="",style="dashed", color="magenta", weight=3];
843 -> 849[label="",style="dashed", color="magenta", weight=3];
836[label="primMinusNatS vuy39 vuy40",fontsize=16,color="burlywood",shape="triangle"];979[label="vuy39/Succ vuy390",fontsize=10,color="white",style="solid",shape="box"];836 -> 979[label="",style="solid", color="burlywood", weight=9];
979 -> 841[label="",style="solid", color="burlywood", weight=3];
980[label="vuy39/Zero",fontsize=10,color="white",style="solid",shape="box"];836 -> 980[label="",style="solid", color="burlywood", weight=9];
980 -> 842[label="",style="solid", color="burlywood", weight=3];
848 -> 836[label="",style="dashed", color="red", weight=0];
848[label="primMinusNatS (Succ vuy52) (Succ vuy53)",fontsize=16,color="magenta"];848 -> 854[label="",style="dashed", color="magenta", weight=3];
848 -> 855[label="",style="dashed", color="magenta", weight=3];
849[label="Succ vuy53",fontsize=16,color="green",shape="box"];841[label="primMinusNatS (Succ vuy390) vuy40",fontsize=16,color="burlywood",shape="box"];982[label="vuy40/Succ vuy400",fontsize=10,color="white",style="solid",shape="box"];841 -> 982[label="",style="solid", color="burlywood", weight=9];
982 -> 844[label="",style="solid", color="burlywood", weight=3];
983[label="vuy40/Zero",fontsize=10,color="white",style="solid",shape="box"];841 -> 983[label="",style="solid", color="burlywood", weight=9];
983 -> 845[label="",style="solid", color="burlywood", weight=3];
842[label="primMinusNatS Zero vuy40",fontsize=16,color="burlywood",shape="box"];984[label="vuy40/Succ vuy400",fontsize=10,color="white",style="solid",shape="box"];842 -> 984[label="",style="solid", color="burlywood", weight=9];
984 -> 846[label="",style="solid", color="burlywood", weight=3];
985[label="vuy40/Zero",fontsize=10,color="white",style="solid",shape="box"];842 -> 985[label="",style="solid", color="burlywood", weight=9];
985 -> 847[label="",style="solid", color="burlywood", weight=3];
854[label="Succ vuy53",fontsize=16,color="green",shape="box"];855[label="Succ vuy52",fontsize=16,color="green",shape="box"];844[label="primMinusNatS (Succ vuy390) (Succ vuy400)",fontsize=16,color="black",shape="box"];844 -> 850[label="",style="solid", color="black", weight=3];
845[label="primMinusNatS (Succ vuy390) Zero",fontsize=16,color="black",shape="box"];845 -> 851[label="",style="solid", color="black", weight=3];
846[label="primMinusNatS Zero (Succ vuy400)",fontsize=16,color="black",shape="box"];846 -> 852[label="",style="solid", color="black", weight=3];
847[label="primMinusNatS Zero Zero",fontsize=16,color="black",shape="box"];847 -> 853[label="",style="solid", color="black", weight=3];
850 -> 836[label="",style="dashed", color="red", weight=0];
850[label="primMinusNatS vuy390 vuy400",fontsize=16,color="magenta"];850 -> 856[label="",style="dashed", color="magenta", weight=3];
850 -> 857[label="",style="dashed", color="magenta", weight=3];
851[label="Succ vuy390",fontsize=16,color="green",shape="box"];852[label="Zero",fontsize=16,color="green",shape="box"];853[label="Zero",fontsize=16,color="green",shape="box"];856[label="vuy400",fontsize=16,color="green",shape="box"];857[label="vuy390",fontsize=16,color="green",shape="box"];}

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                                ↳ QDPSizeChangeProof

                              ↳ QDP

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMinusNatS(Succ(vuy390), Succ(vuy400)) → new_primMinusNatS(vuy390, vuy400)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_primMinusNatS(Succ(vuy390), Succ(vuy400)) → new_primMinusNatS(vuy390, vuy400)
The graph contains the following edges 1 > 1, 2 > 2

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(vuy52, vuy53, Zero, Zero) → new_primDivNatS00(vuy52, vuy53)
new_primDivNatS00(vuy52, vuy53) → new_primDivNatS(new_primMinusNatS0(Succ(vuy52), Succ(vuy53)), Succ(vuy53))
new_primDivNatS0(vuy52, vuy53, Succ(vuy540), Succ(vuy550)) → new_primDivNatS0(vuy52, vuy53, vuy540, vuy550)
new_primDivNatS(Succ(Succ(vuy30000)), Succ(vuy31000)) → new_primDivNatS0(vuy30000, vuy31000, vuy30000, vuy31000)
new_primDivNatS(Succ(Zero), Zero) → new_primDivNatS(new_primMinusNatS2, Zero)
new_primDivNatS0(vuy52, vuy53, Succ(vuy540), Zero) → new_primDivNatS(new_primMinusNatS0(Succ(vuy52), Succ(vuy53)), Succ(vuy53))
new_primDivNatS(Succ(Succ(vuy30000)), Zero) → new_primDivNatS(new_primMinusNatS1(vuy30000), Zero)

The TRS R consists of the following rules:

new_primMinusNatS0(Zero, Succ(vuy400)) → Zero
new_primMinusNatS0(Zero, Zero) → Zero
new_primMinusNatS1(vuy30000) → Succ(vuy30000)
new_primMinusNatS0(Succ(vuy390), Succ(vuy400)) → new_primMinusNatS0(vuy390, vuy400)
new_primMinusNatS0(Succ(vuy390), Zero) → Succ(vuy390)
new_primMinusNatS2 → Zero

The set Q consists of the following terms:

new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS2
new_primMinusNatS0(Succ(x0), Succ(x1))
new_primMinusNatS1(x0)
new_primMinusNatS0(Zero, Zero)
new_primMinusNatS0(Zero, Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 1 less node.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                      ↳ UsableRulesProof

                                    ↳ QDP

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS(Succ(Succ(vuy30000)), Zero) → new_primDivNatS(new_primMinusNatS1(vuy30000), Zero)

The TRS R consists of the following rules:

new_primMinusNatS0(Zero, Succ(vuy400)) → Zero
new_primMinusNatS0(Zero, Zero) → Zero
new_primMinusNatS1(vuy30000) → Succ(vuy30000)
new_primMinusNatS0(Succ(vuy390), Succ(vuy400)) → new_primMinusNatS0(vuy390, vuy400)
new_primMinusNatS0(Succ(vuy390), Zero) → Succ(vuy390)
new_primMinusNatS2 → Zero

The set Q consists of the following terms:

new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS2
new_primMinusNatS0(Succ(x0), Succ(x1))
new_primMinusNatS1(x0)
new_primMinusNatS0(Zero, Zero)
new_primMinusNatS0(Zero, Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                      ↳ UsableRulesProof

                                        ↳ QDP

                                          ↳ QReductionProof

                                    ↳ QDP

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS(Succ(Succ(vuy30000)), Zero) → new_primDivNatS(new_primMinusNatS1(vuy30000), Zero)

The TRS R consists of the following rules:

new_primMinusNatS1(vuy30000) → Succ(vuy30000)

The set Q consists of the following terms:

new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS2
new_primMinusNatS0(Succ(x0), Succ(x1))
new_primMinusNatS1(x0)
new_primMinusNatS0(Zero, Zero)
new_primMinusNatS0(Zero, Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS2
new_primMinusNatS0(Succ(x0), Succ(x1))
new_primMinusNatS0(Zero, Zero)
new_primMinusNatS0(Zero, Succ(x0))

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                      ↳ UsableRulesProof

                                        ↳ QDP

                                          ↳ QReductionProof

                                            ↳ QDP

                                              ↳ RuleRemovalProof

                                    ↳ QDP

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS(Succ(Succ(vuy30000)), Zero) → new_primDivNatS(new_primMinusNatS1(vuy30000), Zero)

The TRS R consists of the following rules:

new_primMinusNatS1(vuy30000) → Succ(vuy30000)

The set Q consists of the following terms:

new_primMinusNatS1(x0)

We have to consider all minimal (P,Q,R)-chains.
By using the rule removal processor [15] with the following polynomial ordering [25], at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

new_primDivNatS(Succ(Succ(vuy30000)), Zero) → new_primDivNatS(new_primMinusNatS1(vuy30000), Zero)

Strictly oriented rules of the TRS R:

new_primMinusNatS1(vuy30000) → Succ(vuy30000)

Used ordering: POLO with Polynomial interpretation [25]:

POL(Succ(x₁)) = 1 + 2·x₁
POL(Zero) = 0
POL(new_primDivNatS(x₁, x₂)) = x₁ + x₂
POL(new_primMinusNatS1(x₁)) = 2 + 2·x₁

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                      ↳ UsableRulesProof

                                        ↳ QDP

                                          ↳ QReductionProof

                                            ↳ QDP

                                              ↳ RuleRemovalProof

                                                ↳ QDP

                                                  ↳ PisEmptyProof

                                    ↳ QDP

                              ↳ QDP

Q DP problem:
P is empty.
R is empty.
The set Q consists of the following terms:

new_primMinusNatS1(x0)

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                    ↳ QDP

                                      ↳ UsableRulesProof

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS00(vuy52, vuy53) → new_primDivNatS(new_primMinusNatS0(Succ(vuy52), Succ(vuy53)), Succ(vuy53))
new_primDivNatS0(vuy52, vuy53, Zero, Zero) → new_primDivNatS00(vuy52, vuy53)
new_primDivNatS0(vuy52, vuy53, Succ(vuy540), Succ(vuy550)) → new_primDivNatS0(vuy52, vuy53, vuy540, vuy550)
new_primDivNatS(Succ(Succ(vuy30000)), Succ(vuy31000)) → new_primDivNatS0(vuy30000, vuy31000, vuy30000, vuy31000)
new_primDivNatS0(vuy52, vuy53, Succ(vuy540), Zero) → new_primDivNatS(new_primMinusNatS0(Succ(vuy52), Succ(vuy53)), Succ(vuy53))

The TRS R consists of the following rules:

new_primMinusNatS0(Zero, Succ(vuy400)) → Zero
new_primMinusNatS0(Zero, Zero) → Zero
new_primMinusNatS1(vuy30000) → Succ(vuy30000)
new_primMinusNatS0(Succ(vuy390), Succ(vuy400)) → new_primMinusNatS0(vuy390, vuy400)
new_primMinusNatS0(Succ(vuy390), Zero) → Succ(vuy390)
new_primMinusNatS2 → Zero

The set Q consists of the following terms:

new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS2
new_primMinusNatS0(Succ(x0), Succ(x1))
new_primMinusNatS1(x0)
new_primMinusNatS0(Zero, Zero)
new_primMinusNatS0(Zero, Succ(x0))

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                    ↳ QDP

                                      ↳ UsableRulesProof

                                        ↳ QDP

                                          ↳ QReductionProof

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS00(vuy52, vuy53) → new_primDivNatS(new_primMinusNatS0(Succ(vuy52), Succ(vuy53)), Succ(vuy53))
new_primDivNatS0(vuy52, vuy53, Zero, Zero) → new_primDivNatS00(vuy52, vuy53)
new_primDivNatS0(vuy52, vuy53, Succ(vuy540), Succ(vuy550)) → new_primDivNatS0(vuy52, vuy53, vuy540, vuy550)
new_primDivNatS(Succ(Succ(vuy30000)), Succ(vuy31000)) → new_primDivNatS0(vuy30000, vuy31000, vuy30000, vuy31000)
new_primDivNatS0(vuy52, vuy53, Succ(vuy540), Zero) → new_primDivNatS(new_primMinusNatS0(Succ(vuy52), Succ(vuy53)), Succ(vuy53))

The TRS R consists of the following rules:

new_primMinusNatS0(Succ(vuy390), Succ(vuy400)) → new_primMinusNatS0(vuy390, vuy400)
new_primMinusNatS0(Zero, Succ(vuy400)) → Zero
new_primMinusNatS0(Zero, Zero) → Zero
new_primMinusNatS0(Succ(vuy390), Zero) → Succ(vuy390)

The set Q consists of the following terms:

new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS2
new_primMinusNatS0(Succ(x0), Succ(x1))
new_primMinusNatS1(x0)
new_primMinusNatS0(Zero, Zero)
new_primMinusNatS0(Zero, Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primMinusNatS2
new_primMinusNatS1(x0)

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                    ↳ QDP

                                      ↳ UsableRulesProof

                                        ↳ QDP

                                          ↳ QReductionProof

                                            ↳ QDP

                                              ↳ Rewriting

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(vuy52, vuy53, Zero, Zero) → new_primDivNatS00(vuy52, vuy53)
new_primDivNatS00(vuy52, vuy53) → new_primDivNatS(new_primMinusNatS0(Succ(vuy52), Succ(vuy53)), Succ(vuy53))
new_primDivNatS(Succ(Succ(vuy30000)), Succ(vuy31000)) → new_primDivNatS0(vuy30000, vuy31000, vuy30000, vuy31000)
new_primDivNatS0(vuy52, vuy53, Succ(vuy540), Succ(vuy550)) → new_primDivNatS0(vuy52, vuy53, vuy540, vuy550)
new_primDivNatS0(vuy52, vuy53, Succ(vuy540), Zero) → new_primDivNatS(new_primMinusNatS0(Succ(vuy52), Succ(vuy53)), Succ(vuy53))

The TRS R consists of the following rules:

new_primMinusNatS0(Succ(vuy390), Succ(vuy400)) → new_primMinusNatS0(vuy390, vuy400)
new_primMinusNatS0(Zero, Succ(vuy400)) → Zero
new_primMinusNatS0(Zero, Zero) → Zero
new_primMinusNatS0(Succ(vuy390), Zero) → Succ(vuy390)

The set Q consists of the following terms:

new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Succ(x0), Succ(x1))
new_primMinusNatS0(Zero, Zero)
new_primMinusNatS0(Zero, Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule new_primDivNatS00(vuy52, vuy53) → new_primDivNatS(new_primMinusNatS0(Succ(vuy52), Succ(vuy53)), Succ(vuy53)) at position [0] we obtained the following new rules:

new_primDivNatS00(vuy52, vuy53) → new_primDivNatS(new_primMinusNatS0(vuy52, vuy53), Succ(vuy53))

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                    ↳ QDP

                                      ↳ UsableRulesProof

                                        ↳ QDP

                                          ↳ QReductionProof

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ Rewriting

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(vuy52, vuy53, Zero, Zero) → new_primDivNatS00(vuy52, vuy53)
new_primDivNatS00(vuy52, vuy53) → new_primDivNatS(new_primMinusNatS0(vuy52, vuy53), Succ(vuy53))
new_primDivNatS0(vuy52, vuy53, Succ(vuy540), Succ(vuy550)) → new_primDivNatS0(vuy52, vuy53, vuy540, vuy550)
new_primDivNatS(Succ(Succ(vuy30000)), Succ(vuy31000)) → new_primDivNatS0(vuy30000, vuy31000, vuy30000, vuy31000)
new_primDivNatS0(vuy52, vuy53, Succ(vuy540), Zero) → new_primDivNatS(new_primMinusNatS0(Succ(vuy52), Succ(vuy53)), Succ(vuy53))

The TRS R consists of the following rules:

new_primMinusNatS0(Succ(vuy390), Succ(vuy400)) → new_primMinusNatS0(vuy390, vuy400)
new_primMinusNatS0(Zero, Succ(vuy400)) → Zero
new_primMinusNatS0(Zero, Zero) → Zero
new_primMinusNatS0(Succ(vuy390), Zero) → Succ(vuy390)

The set Q consists of the following terms:

new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Succ(x0), Succ(x1))
new_primMinusNatS0(Zero, Zero)
new_primMinusNatS0(Zero, Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule new_primDivNatS0(vuy52, vuy53, Succ(vuy540), Zero) → new_primDivNatS(new_primMinusNatS0(Succ(vuy52), Succ(vuy53)), Succ(vuy53)) at position [0] we obtained the following new rules:

new_primDivNatS0(vuy52, vuy53, Succ(vuy540), Zero) → new_primDivNatS(new_primMinusNatS0(vuy52, vuy53), Succ(vuy53))

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                    ↳ QDP

                                      ↳ UsableRulesProof

                                        ↳ QDP

                                          ↳ QReductionProof

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ QDPOrderProof

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(vuy52, vuy53, Zero, Zero) → new_primDivNatS00(vuy52, vuy53)
new_primDivNatS(Succ(Succ(vuy30000)), Succ(vuy31000)) → new_primDivNatS0(vuy30000, vuy31000, vuy30000, vuy31000)
new_primDivNatS0(vuy52, vuy53, Succ(vuy540), Succ(vuy550)) → new_primDivNatS0(vuy52, vuy53, vuy540, vuy550)
new_primDivNatS00(vuy52, vuy53) → new_primDivNatS(new_primMinusNatS0(vuy52, vuy53), Succ(vuy53))
new_primDivNatS0(vuy52, vuy53, Succ(vuy540), Zero) → new_primDivNatS(new_primMinusNatS0(vuy52, vuy53), Succ(vuy53))

The TRS R consists of the following rules:

new_primMinusNatS0(Succ(vuy390), Succ(vuy400)) → new_primMinusNatS0(vuy390, vuy400)
new_primMinusNatS0(Zero, Succ(vuy400)) → Zero
new_primMinusNatS0(Zero, Zero) → Zero
new_primMinusNatS0(Succ(vuy390), Zero) → Succ(vuy390)

The set Q consists of the following terms:

new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Succ(x0), Succ(x1))
new_primMinusNatS0(Zero, Zero)
new_primMinusNatS0(Zero, Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

new_primDivNatS(Succ(Succ(vuy30000)), Succ(vuy31000)) → new_primDivNatS0(vuy30000, vuy31000, vuy30000, vuy31000)

The remaining pairs can at least be oriented weakly.

new_primDivNatS0(vuy52, vuy53, Zero, Zero) → new_primDivNatS00(vuy52, vuy53)
new_primDivNatS0(vuy52, vuy53, Succ(vuy540), Succ(vuy550)) → new_primDivNatS0(vuy52, vuy53, vuy540, vuy550)
new_primDivNatS00(vuy52, vuy53) → new_primDivNatS(new_primMinusNatS0(vuy52, vuy53), Succ(vuy53))
new_primDivNatS0(vuy52, vuy53, Succ(vuy540), Zero) → new_primDivNatS(new_primMinusNatS0(vuy52, vuy53), Succ(vuy53))

Used ordering: Polynomial interpretation [25]:

POL(Succ(x₁)) = 1 + x₁
POL(Zero) = 0
POL(new_primDivNatS(x₁, x₂)) = x₁
POL(new_primDivNatS0(x₁, x₂, x₃, x₄)) = x₁
POL(new_primDivNatS00(x₁, x₂)) = x₁
POL(new_primMinusNatS0(x₁, x₂)) = x₁

The following usable rules [17] were oriented:

new_primMinusNatS0(Succ(vuy390), Succ(vuy400)) → new_primMinusNatS0(vuy390, vuy400)
new_primMinusNatS0(Zero, Zero) → Zero
new_primMinusNatS0(Succ(vuy390), Zero) → Succ(vuy390)
new_primMinusNatS0(Zero, Succ(vuy400)) → Zero

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                    ↳ QDP

                                      ↳ UsableRulesProof

                                        ↳ QDP

                                          ↳ QReductionProof

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ QDPOrderProof

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(vuy52, vuy53, Zero, Zero) → new_primDivNatS00(vuy52, vuy53)
new_primDivNatS00(vuy52, vuy53) → new_primDivNatS(new_primMinusNatS0(vuy52, vuy53), Succ(vuy53))
new_primDivNatS0(vuy52, vuy53, Succ(vuy540), Succ(vuy550)) → new_primDivNatS0(vuy52, vuy53, vuy540, vuy550)
new_primDivNatS0(vuy52, vuy53, Succ(vuy540), Zero) → new_primDivNatS(new_primMinusNatS0(vuy52, vuy53), Succ(vuy53))

The TRS R consists of the following rules:

new_primMinusNatS0(Succ(vuy390), Succ(vuy400)) → new_primMinusNatS0(vuy390, vuy400)
new_primMinusNatS0(Zero, Succ(vuy400)) → Zero
new_primMinusNatS0(Zero, Zero) → Zero
new_primMinusNatS0(Succ(vuy390), Zero) → Succ(vuy390)

The set Q consists of the following terms:

new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Succ(x0), Succ(x1))
new_primMinusNatS0(Zero, Zero)
new_primMinusNatS0(Zero, Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 3 less nodes.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                    ↳ QDP

                                      ↳ UsableRulesProof

                                        ↳ QDP

                                          ↳ QReductionProof

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ QDPOrderProof

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                                                            ↳ QDP

                                                              ↳ UsableRulesProof

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(vuy52, vuy53, Succ(vuy540), Succ(vuy550)) → new_primDivNatS0(vuy52, vuy53, vuy540, vuy550)

The TRS R consists of the following rules:

new_primMinusNatS0(Succ(vuy390), Succ(vuy400)) → new_primMinusNatS0(vuy390, vuy400)
new_primMinusNatS0(Zero, Succ(vuy400)) → Zero
new_primMinusNatS0(Zero, Zero) → Zero
new_primMinusNatS0(Succ(vuy390), Zero) → Succ(vuy390)

The set Q consists of the following terms:

new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Succ(x0), Succ(x1))
new_primMinusNatS0(Zero, Zero)
new_primMinusNatS0(Zero, Succ(x0))

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                    ↳ QDP

                                      ↳ UsableRulesProof

                                        ↳ QDP

                                          ↳ QReductionProof

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ QDPOrderProof

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                                                            ↳ QDP

                                                              ↳ UsableRulesProof

                                                                ↳ QDP

                                                                  ↳ QReductionProof

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(vuy52, vuy53, Succ(vuy540), Succ(vuy550)) → new_primDivNatS0(vuy52, vuy53, vuy540, vuy550)

R is empty.
The set Q consists of the following terms:

new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Succ(x0), Succ(x1))
new_primMinusNatS0(Zero, Zero)
new_primMinusNatS0(Zero, Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_primMinusNatS0(Succ(x0), Zero)
new_primMinusNatS0(Succ(x0), Succ(x1))
new_primMinusNatS0(Zero, Zero)
new_primMinusNatS0(Zero, Succ(x0))

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                                ↳ DependencyGraphProof

                                  ↳ AND

                                    ↳ QDP

                                    ↳ QDP

                                      ↳ UsableRulesProof

                                        ↳ QDP

                                          ↳ QReductionProof

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ QDPOrderProof

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                                                            ↳ QDP

                                                              ↳ UsableRulesProof

                                                                ↳ QDP

                                                                  ↳ QReductionProof

                                                                    ↳ QDP

                                                                      ↳ QDPSizeChangeProof

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primDivNatS0(vuy52, vuy53, Succ(vuy540), Succ(vuy550)) → new_primDivNatS0(vuy52, vuy53, vuy540, vuy550)

From the DPs we obtained the following set of size-change graphs:

new_primDivNatS0(vuy52, vuy53, Succ(vuy540), Succ(vuy550)) → new_primDivNatS0(vuy52, vuy53, vuy540, vuy550)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 > 4

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ IFR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                                ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_primMinusNat(vuy39, vuy40, Succ(vuy410), Succ(vuy420)) → new_primMinusNat(vuy39, vuy40, vuy410, vuy420)

From the DPs we obtained the following set of size-change graphs:

new_primMinusNat(vuy39, vuy40, Succ(vuy410), Succ(vuy420)) → new_primMinusNat(vuy39, vuy40, vuy410, vuy420)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 > 4

primDivNatS0	x y True	= Succ (primDivNatS (primMinusNatS x y) (Succ y))
primDivNatS0	x y False	= Zero

primModNatS0	x y True	= primModNatS (primMinusNatS x y) (Succ y)
primModNatS0	x y False	= Succ x

toEnum	zx	= toEnum11 zx
toEnum	yz	= toEnum9 yz
toEnum	yy	= toEnum7 yy